src/Pure/Isar/local_theory.ML
changeset 36610 bafd82950e24
parent 36451 ddc965e172c4
child 37949 48a874444164
     1.1 --- a/src/Pure/Isar/local_theory.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -181,7 +181,8 @@
     1.4    Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
     1.5  
     1.6  fun target_morphism lthy = standard_morphism lthy (target_of lthy);
     1.7 -fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
     1.8 +fun global_morphism lthy =
     1.9 +  standard_morphism lthy (ProofContext.init_global (ProofContext.theory_of lthy));
    1.10  
    1.11  
    1.12  (* primitive operations *)
    1.13 @@ -270,7 +271,7 @@
    1.14  fun exit_result_global f (x, lthy) =
    1.15    let
    1.16      val thy = exit_global lthy;
    1.17 -    val thy_ctxt = ProofContext.init thy;
    1.18 +    val thy_ctxt = ProofContext.init_global thy;
    1.19      val phi = standard_morphism lthy thy_ctxt;
    1.20    in (f phi x, thy) end;
    1.21