src/Pure/Isar/class.ML
changeset 36610 bafd82950e24
parent 36464 b789c1731fb7
child 36645 30bd207ec222
     1.1 --- a/src/Pure/Isar/class.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5  fun calculate thy class sups base_sort param_map assm_axiom =
     1.6    let
     1.7 -    val empty_ctxt = ProofContext.init thy;
     1.8 +    val empty_ctxt = ProofContext.init_global thy;
     1.9  
    1.10      (* instantiation of canonical interpretation *)
    1.11      val aT = TFree (Name.aT, base_sort);
    1.12 @@ -143,7 +143,7 @@
    1.13        #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    1.14      val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.15        Expression.Positional []))) sups, []);
    1.16 -    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
    1.17 +    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
    1.18        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.19      fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
    1.20        | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
    1.21 @@ -194,7 +194,7 @@
    1.22      val sup_sort = inter_sort base_sort sups;
    1.23  
    1.24      (* process elements as class specification *)
    1.25 -    val class_ctxt = begin sups base_sort (ProofContext.init thy);
    1.26 +    val class_ctxt = begin sups base_sort (ProofContext.init_global thy);
    1.27      val ((_, _, syntax_elems), _) = class_ctxt
    1.28        |> Expression.cert_declaration supexpr I inferred_elems;
    1.29      fun check_vars e vs = if null vs
    1.30 @@ -340,7 +340,7 @@
    1.31  
    1.32  val subclass = gen_subclass (K I) user_proof;
    1.33  fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
    1.34 -val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init) user_proof;
    1.35 +val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
    1.36  
    1.37  end; (*local*)
    1.38