diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 3bb3b21fd053df8c75c19b6e7835bfe8532fa5c4..45bdd477a8fa0e572ff6655507440f012cc5fca0 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1657,10 +1657,11 @@ logic_def:
       exit_type_variables_scope ();
       LDpredicate_def (id, labels, tvars, $3, $5) }
 /* inductive predicate definition */
-| INDUCTIVE poly_id parameters LBRACE indcases RBRACE
-    { let (id,labels,tvars) = $2 in
-      exit_type_variables_scope ();
-      LDinductive_def(id, labels, tvars, $3, $5) }
+| INDUCTIVE pred = poly_id params = parameters
+    midrule({exit_type_variables_scope()})
+    LBRACE cases = indcases RBRACE
+    { let (id,labels,tvars) = pred in
+      LDinductive_def(id, labels, tvars, params, cases) }
 | LEMMA poly_id COLON lexpr SEMICOLON
     { let (id,labels,tvars) = $2 in
       exit_type_variables_scope ();
diff --git a/tests/spec/oracle/polymorphic_inductive.res.oracle b/tests/spec/oracle/polymorphic_inductive.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f003162d035a68df660507c0df1a4a579ca6e527
--- /dev/null
+++ b/tests/spec/oracle/polymorphic_inductive.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing polymorphic_inductive.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+inductive P<A>(A i, \list<A>  s) {
+  case one<A>: ∀ A a, \list<A>  s; \Cons(a, s) ≡ [| a |] ⇒ P(a, s);
+  }
+ */
+
diff --git a/tests/spec/polymorphic_inductive.i b/tests/spec/polymorphic_inductive.i
new file mode 100644
index 0000000000000000000000000000000000000000..c972f6c494a69c7129bc8a8e72fce8c64591f51f
--- /dev/null
+++ b/tests/spec/polymorphic_inductive.i
@@ -0,0 +1,5 @@
+/*@ inductive P<A>(A i, \list<A> s){
+    case one<A>: 
+      \forall A a, \list<A> s ; \Cons(a, s) == [| a |] ==> P(a, s);
+    }
+*/