src/HOL/Nominal/nominal_inductive2.ML
changeset 30763 6976521b4263
parent 30450 7655e6533209
child 31174 f1f1e9b53c81
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:21:49 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:53:33 2009 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4        | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
     1.5      fun mk_avoids params name sets =
     1.6        let
     1.7 -        val (_, ctxt') = ProofContext.add_fixes_i
     1.8 +        val (_, ctxt') = ProofContext.add_fixes
     1.9            (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
    1.10          fun mk s =
    1.11            let