src/ZF/Tools/inductive_package.ML
changeset 42359 6ca5407863ed
parent 42290 b1f544c84040
child 42361 23f352990944
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4      If no mutual recursion then it equals the one recursive set.
     1.5      If mutual recursion then it differs from all the recursive sets. *)
     1.6    val big_rec_base_name = space_implode "_" rec_base_names;
     1.7 -  val big_rec_name = Sign.intern_const thy big_rec_base_name;
     1.8 +  val big_rec_name = ProofContext.intern_const ctxt big_rec_base_name;
     1.9  
    1.10  
    1.11    val _ =