src/Pure/Isar/class_declaration.ML
changeset 57181 2d13bf9ea77b
parent 56921 5bf71b4da706
child 57182 79d43c510b84
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Jun 06 12:36:06 2014 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Fri Jun 06 19:19:46 2014 +0200
     1.3 @@ -6,14 +6,14 @@
     1.4  
     1.5  signature CLASS_DECLARATION =
     1.6  sig
     1.7 -  val class: (local_theory -> local_theory) -> binding -> class list ->
     1.8 +  val class: binding -> class list ->
     1.9      Element.context_i list -> theory -> string * local_theory
    1.10 -  val class_cmd: (local_theory -> local_theory) -> binding -> xstring list ->
    1.11 +  val class_cmd: binding -> xstring list ->
    1.12      Element.context list -> theory -> string * local_theory
    1.13 -  val prove_subclass: (local_theory -> local_theory) -> tactic -> class ->
    1.14 +  val prove_subclass: tactic -> class ->
    1.15      local_theory -> local_theory
    1.16 -  val subclass: (local_theory -> local_theory) -> class -> local_theory -> Proof.state
    1.17 -  val subclass_cmd: (local_theory -> local_theory) -> xstring -> local_theory -> Proof.state
    1.18 +  val subclass: class -> local_theory -> Proof.state
    1.19 +  val subclass_cmd: xstring -> local_theory -> Proof.state
    1.20  end;
    1.21  
    1.22  structure Class_Declaration: CLASS_DECLARATION =
    1.23 @@ -306,7 +306,7 @@
    1.24      #> pair (param_map, params, assm_axiom)))
    1.25    end;
    1.26  
    1.27 -fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
    1.28 +fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
    1.29    let
    1.30      val class = Sign.full_name thy b;
    1.31      val prefix = Binding.qualify true "class";
    1.32 @@ -314,7 +314,7 @@
    1.33        prep_class_spec thy raw_supclasses raw_elems;
    1.34    in
    1.35      thy
    1.36 -    |> Expression.add_locale I b (prefix b) supexpr elems
    1.37 +    |> Expression.add_locale b (prefix b) supexpr elems
    1.38      |> snd |> Local_Theory.exit_global
    1.39      |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
    1.40      |-> (fn (param_map, params, assm_axiom) =>
    1.41 @@ -325,7 +325,7 @@
    1.42      #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
    1.43      #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
    1.44      |> snd
    1.45 -    |> Named_Target.init before_exit class
    1.46 +    |> Named_Target.init class
    1.47      |> pair class
    1.48    end;
    1.49  
    1.50 @@ -342,7 +342,7 @@
    1.51  
    1.52  local
    1.53  
    1.54 -fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
    1.55 +fun gen_subclass prep_class do_proof raw_sup lthy =
    1.56    let
    1.57      val thy = Proof_Context.theory_of lthy;
    1.58      val proto_sup = prep_class thy raw_sup;
    1.59 @@ -371,7 +371,7 @@
    1.60  
    1.61  in
    1.62  
    1.63 -fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
    1.64 +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
    1.65  
    1.66  fun subclass x = gen_subclass (K I) user_proof x;
    1.67  fun subclass_cmd x =