src/HOL/Nominal/nominal_inductive.ML
changeset 36323 655e2d74de3a
parent 35232 f588e1169c8b
child 36428 874843c1e96e
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 15:13:33 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Apr 25 15:52:03 2010 +0200
     1.3 @@ -543,7 +543,7 @@
     1.4  
     1.5    in
     1.6      ctxt'' |>
     1.7 -    Proof.theorem_i NONE (fn thss => fn ctxt =>
     1.8 +    Proof.theorem NONE (fn thss => fn ctxt =>
     1.9        let
    1.10          val rec_name = space_implode "_" (map Long_Name.base_name names);
    1.11          val rec_qualified = Binding.qualify false rec_name;