src/HOL/Tools/recdef.ML
changeset 36610 bafd82950e24
parent 35756 cfde251d03a5
child 36865 7330e4eefbd7
     1.1 --- a/src/HOL/Tools/recdef.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/recdef.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4  
     1.5  fun prepare_hints thy opt_src =
     1.6    let
     1.7 -    val ctxt0 = ProofContext.init thy;
     1.8 +    val ctxt0 = ProofContext.init_global thy;
     1.9      val ctxt =
    1.10        (case opt_src of
    1.11          NONE => ctxt0
    1.12 @@ -172,7 +172,7 @@
    1.13  
    1.14  fun prepare_hints_i thy () =
    1.15    let
    1.16 -    val ctxt0 = ProofContext.init thy;
    1.17 +    val ctxt0 = ProofContext.init_global thy;
    1.18      val {simps, congs, wfs} = get_global_hints thy;
    1.19    in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
    1.20  
    1.21 @@ -234,7 +234,7 @@
    1.22      val _ = requires_recdef thy;
    1.23      val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
    1.24  
    1.25 -    val congs = eval_thms (ProofContext.init thy) raw_congs;
    1.26 +    val congs = eval_thms (ProofContext.init_global thy) raw_congs;
    1.27      val (thy2, induct_rules) = tfl_fn thy congs name eqs;
    1.28      val ([induct_rules'], thy3) =
    1.29        thy2