src/HOL/Tools/old_primrec.ML
changeset 36610 bafd82950e24
parent 35845 e5980f0ad025
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -214,7 +214,7 @@
     1.4                                  fs @ map Bound (0 ::(length ls downto 1))))
     1.5      val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
     1.6      val def_prop =
     1.7 -      singleton (Syntax.check_terms (ProofContext.init thy))
     1.8 +      singleton (Syntax.check_terms (ProofContext.init_global thy))
     1.9          (Logic.mk_equals (Const (fname, dummyT), rhs));
    1.10    in (def_name, def_prop) end;
    1.11