src/Pure/Isar/class_declaration.ML
changeset 42360 da8817d01e7c
parent 42357 3305f573294e
child 42375 774df7c59508
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -27,7 +27,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_global thy;
     1.8 +    val empty_ctxt = Proof_Context.init_global thy;
     1.9  
    1.10      (* instantiation of canonical interpretation *)
    1.11      val aT = TFree (Name.aT, base_sort);
    1.12 @@ -55,7 +55,7 @@
    1.13            of (_, NONE) => all_tac
    1.14             | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
    1.15          val tac = loc_intro_tac
    1.16 -          THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
    1.17 +          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom))
    1.18        in Element.prove_witness empty_ctxt prop tac end) prop;
    1.19      val axiom = Option.map Element.conclude_witness wit;
    1.20  
    1.21 @@ -73,7 +73,7 @@
    1.22           of SOME eq_morph => const_morph $> eq_morph
    1.23            | NONE => const_morph
    1.24          val thm'' = Morphism.thm const_eq_morph thm';
    1.25 -        val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
    1.26 +        val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    1.27        in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.28      val assm_intro = Option.map prove_assm_intro
    1.29        (fst (Locale.intros_of thy class));
    1.30 @@ -146,11 +146,11 @@
    1.31      (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.32      val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.33        Expression.Positional []))) sups, []);
    1.34 -    val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    1.35 +    val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    1.36        #> Class.redeclare_operations thy sups
    1.37        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    1.38        #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    1.39 -    val ((raw_supparams, _, raw_inferred_elems), _) = ProofContext.init_global thy
    1.40 +    val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
    1.41        |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
    1.42        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.43      fun filter_element (Element.Fixes []) = NONE
    1.44 @@ -207,7 +207,7 @@
    1.45      val sup_sort = inter_sort base_sort sups;
    1.46  
    1.47      (* process elements as class specification *)
    1.48 -    val class_ctxt = Class.begin sups base_sort (ProofContext.init_global thy);
    1.49 +    val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
    1.50      val ((_, _, syntax_elems), _) = class_ctxt
    1.51        |> Expression.cert_declaration supexpr I inferred_elems;
    1.52      fun check_vars e vs = if null vs
    1.53 @@ -324,7 +324,7 @@
    1.54  
    1.55  fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
    1.56    let
    1.57 -    val thy = ProofContext.theory_of lthy;
    1.58 +    val thy = Proof_Context.theory_of lthy;
    1.59      val proto_sup = prep_class thy raw_sup;
    1.60      val proto_sub = case Named_Target.peek lthy
    1.61       of SOME {target, is_class = true, ...} => target
    1.62 @@ -337,9 +337,9 @@
    1.63      val some_prop = try the_single props;
    1.64      val some_dep_morph = try the_single (map snd deps);
    1.65      fun after_qed some_wit =
    1.66 -      ProofContext.background_theory (Class.register_subclass (sub, sup)
    1.67 +      Proof_Context.background_theory (Class.register_subclass (sub, sup)
    1.68          some_dep_morph some_wit export)
    1.69 -      #> ProofContext.theory_of #> Named_Target.init before_exit sub;
    1.70 +      #> Proof_Context.theory_of #> Named_Target.init before_exit sub;
    1.71    in do_proof after_qed some_prop goal_ctxt end;
    1.72  
    1.73  fun user_proof after_qed some_prop =
    1.74 @@ -354,7 +354,7 @@
    1.75  
    1.76  val subclass = gen_subclass (K I) user_proof;
    1.77  fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
    1.78 -val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
    1.79 +val subclass_cmd = gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof;
    1.80  
    1.81  end; (*local*)
    1.82