src/Pure/Isar/class_declaration.ML
changeset 41585 45d7da4e4ccf
parent 40188 eddda8e38360
child 42357 3305f573294e
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Jan 15 22:40:17 2011 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sun Jan 16 14:57:14 2011 +0100
     1.3 @@ -6,13 +6,14 @@
     1.4  
     1.5  signature CLASS_DECLARATION =
     1.6  sig
     1.7 -  val class: binding -> class list -> Element.context_i list
     1.8 -    -> theory -> string * local_theory
     1.9 -  val class_cmd: binding -> xstring list -> Element.context list
    1.10 -    -> theory -> string * local_theory
    1.11 -  val prove_subclass: tactic -> class -> local_theory -> local_theory
    1.12 -  val subclass: class -> local_theory -> Proof.state
    1.13 -  val subclass_cmd: xstring -> local_theory -> Proof.state
    1.14 +  val class: (local_theory -> local_theory) -> binding -> class list ->
    1.15 +    Element.context_i list -> theory -> string * local_theory
    1.16 +  val class_cmd: (local_theory -> local_theory) -> binding -> xstring list ->
    1.17 +    Element.context list -> theory -> string * local_theory
    1.18 +  val prove_subclass: (local_theory -> local_theory) -> tactic -> class ->
    1.19 +    local_theory -> local_theory
    1.20 +  val subclass: (local_theory -> local_theory) -> class -> local_theory -> Proof.state
    1.21 +  val subclass_cmd: (local_theory -> local_theory) -> xstring -> local_theory -> Proof.state
    1.22  end;
    1.23  
    1.24  structure Class_Declaration: CLASS_DECLARATION =
    1.25 @@ -288,14 +289,14 @@
    1.26      #> pair (param_map, params, assm_axiom)))
    1.27    end;
    1.28  
    1.29 -fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
    1.30 +fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
    1.31    let
    1.32      val class = Sign.full_name thy b;
    1.33      val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
    1.34        prep_class_spec thy raw_supclasses raw_elems;
    1.35    in
    1.36      thy
    1.37 -    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
    1.38 +    |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems
    1.39      |> snd |> Local_Theory.exit_global
    1.40      |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
    1.41      ||> Theory.checkpoint
    1.42 @@ -305,7 +306,7 @@
    1.43         Context.theory_map (Locale.add_registration (class, base_morph)
    1.44           (Option.map (rpair true) eq_morph) export_morph)
    1.45      #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.46 -    |> Named_Target.init class
    1.47 +    |> Named_Target.init before_exit class
    1.48      |> pair class
    1.49    end;
    1.50  
    1.51 @@ -321,7 +322,7 @@
    1.52  
    1.53  local
    1.54  
    1.55 -fun gen_subclass prep_class do_proof raw_sup lthy =
    1.56 +fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
    1.57    let
    1.58      val thy = ProofContext.theory_of lthy;
    1.59      val proto_sup = prep_class thy raw_sup;
    1.60 @@ -338,7 +339,7 @@
    1.61      fun after_qed some_wit =
    1.62        ProofContext.background_theory (Class.register_subclass (sub, sup)
    1.63          some_dep_morph some_wit export)
    1.64 -      #> ProofContext.theory_of #> Named_Target.init sub;
    1.65 +      #> ProofContext.theory_of #> Named_Target.init before_exit sub;
    1.66    in do_proof after_qed some_prop goal_ctxt end;
    1.67  
    1.68  fun user_proof after_qed some_prop =
    1.69 @@ -352,7 +353,7 @@
    1.70  in
    1.71  
    1.72  val subclass = gen_subclass (K I) user_proof;
    1.73 -fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
    1.74 +fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
    1.75  val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
    1.76  
    1.77  end; (*local*)