# HG changeset patch # User haftmann # Date 1388007329 -3600 # Node ID 7b9a67cbd48f189cf391a69b5f60ef0339b746e3 # Parent 82bfac35f16fbb829940a711e7d541a01eb21546 self-contained formulation of subclass command, avoiding hard-wired Named_Target.init diff -r 82bfac35f16f -r 7b9a67cbd48f src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Dec 25 22:35:28 2013 +0100 +++ b/src/Pure/Isar/class.ML Wed Dec 25 22:35:29 2013 +0100 @@ -44,7 +44,7 @@ val classrel: class * class -> theory -> Proof.state val classrel_cmd: xstring * xstring -> theory -> Proof.state val register_subclass: class * class -> morphism option -> Element.witness option - -> morphism -> theory -> theory + -> morphism -> local_theory -> local_theory (*tactics*) val intro_classes_tac: thm list -> tactic @@ -245,30 +245,6 @@ |> activate_defs class (the_list some_def) end; -fun register_subclass (sub, sup) some_dep_morph some_witn export thy = - let - val intros = (snd o rules thy) sup :: map_filter I - [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_witn, - (fst o rules thy) sub]; - val classrel = - Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup)) - (K (EVERY (map (TRYALL o rtac) intros))); - val diff_sort = Sign.complete_sort thy [sup] - |> subtract (op =) (Sign.complete_sort thy [sub]) - |> filter (is_class thy); - val add_dependency = - (case some_dep_morph of - SOME dep_morph => Locale.add_dependency sub - (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export - | NONE => I); - in - thy - |> Axclass.add_classrel classrel - |> Class_Data.map (Graph.add_edge (sub, sup)) - |> activate_defs sub (these_defs thy diff_sort) - |> add_dependency - end; - (** classes and class target **) @@ -314,6 +290,11 @@ |> Overloading.set_primary_constraints end; +fun synchronize_class_syntax_target class lthy = + lthy + |> Local_Theory.map_contexts + (K (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class))); + fun redeclare_operations thy sort = fold (redeclare_const thy o fst) (these_operations thy sort); @@ -336,11 +317,9 @@ local -fun target_extension f class lthy = - lthy - |> Local_Theory.raw_theory f - |> Local_Theory.map_contexts - (K (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class))); +fun target_extension f class = + Local_Theory.raw_theory f + #> synchronize_class_syntax_target class; fun target_const class ((c, mx), (type_params, term_params, dict)) thy = let @@ -394,7 +373,33 @@ end; -(* simple subclasses *) +(* subclasses *) + +fun register_subclass (sub, sup) some_dep_morph some_witn export lthy = + let + val thy = Proof_Context.theory_of lthy; + val intros = (snd o rules thy) sup :: map_filter I + [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_witn, + (fst o rules thy) sub]; + val classrel = + Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup)) + (K (EVERY (map (TRYALL o rtac) intros))); + val diff_sort = Sign.complete_sort thy [sup] + |> subtract (op =) (Sign.complete_sort thy [sub]) + |> filter (is_class thy); + fun add_dependency some_wit = case some_dep_morph of + SOME dep_morph => Generic_Target.locale_dependency sub + (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export + | NONE => I; + in + lthy + |> Local_Theory.raw_theory + (Axclass.add_classrel classrel + #> Class_Data.map (Graph.add_edge (sub, sup)) + #> activate_defs sub (these_defs thy diff_sort)) + |> add_dependency some_witn + |> synchronize_class_syntax_target sub + end; local diff -r 82bfac35f16f -r 7b9a67cbd48f src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Dec 25 22:35:28 2013 +0100 +++ b/src/Pure/Isar/class_declaration.ML Wed Dec 25 22:35:29 2013 +0100 @@ -355,9 +355,7 @@ val some_prop = try the_single props; val some_dep_morph = try the_single (map snd deps); fun after_qed some_wit = - Proof_Context.background_theory (Class.register_subclass (sub, sup) - some_dep_morph some_wit export) - #> Proof_Context.theory_of #> Named_Target.init before_exit sub; + Class.register_subclass (sub, sup) some_dep_morph some_wit export; in do_proof after_qed some_prop goal_ctxt end; fun user_proof after_qed some_prop =