src/Pure/Isar/theory_target.ML
changeset 36610 bafd82950e24
parent 36106 19deea200358
child 37146 f652333bbf8e
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4  fun import_export_proof ctxt (name, raw_th) =
     1.5    let
     1.6      val thy = ProofContext.theory_of ctxt;
     1.7 -    val thy_ctxt = ProofContext.init thy;
     1.8 +    val thy_ctxt = ProofContext.init_global thy;
     1.9      val certT = Thm.ctyp_of thy;
    1.10      val cert = Thm.cterm_of thy;
    1.11  
    1.12 @@ -213,7 +213,7 @@
    1.13  
    1.14  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
    1.15    let
    1.16 -    val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.17 +    val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
    1.18      val target_ctxt = Local_Theory.target_of lthy;
    1.19  
    1.20      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.21 @@ -286,7 +286,7 @@
    1.22  fun define ta ((b, mx), ((name, atts), rhs)) lthy =
    1.23    let
    1.24      val thy = ProofContext.theory_of lthy;
    1.25 -    val thy_ctxt = ProofContext.init thy;
    1.26 +    val thy_ctxt = ProofContext.init_global thy;
    1.27  
    1.28      val name' = Thm.def_binding_optional b name;
    1.29  
    1.30 @@ -342,7 +342,7 @@
    1.31  fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
    1.32    if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
    1.33    else if not (null overloading) then Overloading.init overloading
    1.34 -  else if not is_locale then ProofContext.init
    1.35 +  else if not is_locale then ProofContext.init_global
    1.36    else if not is_class then Locale.init target
    1.37    else Class_Target.init target;
    1.38  
    1.39 @@ -364,7 +364,7 @@
    1.40  
    1.41  fun gen_overloading prep_const raw_ops thy =
    1.42    let
    1.43 -    val ctxt = ProofContext.init thy;
    1.44 +    val ctxt = ProofContext.init_global thy;
    1.45      val ops = raw_ops |> map (fn (name, const, checked) =>
    1.46        (name, Term.dest_Const (prep_const ctxt const), checked));
    1.47    in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;