# HG changeset patch # User wenzelm # Date 1126018796 -7200 # Node ID 3b9ff0131ed1e3e97db258b55662a09cd29b3c39 # Parent a6917ddc864f69053ba7ed513c4b48d4fa7de59d name space prefix is now "c_class" instead of just "c"; export get_info; tuned; diff -r a6917ddc864f -r 3b9ff0131ed1 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Sep 06 16:59:55 2005 +0200 +++ b/src/Pure/axclass.ML Tue Sep 06 16:59:56 2005 +0200 @@ -9,6 +9,7 @@ sig val quiet_mode: bool ref val print_axclasses: theory -> unit + val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list} val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list -> theory -> theory * {intro: thm, axioms: thm list} val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list @@ -70,7 +71,6 @@ (* names *) -fun intro_name c = c ^ "I"; val introN = "intro"; val axiomsN = "axioms"; @@ -153,23 +153,20 @@ (* get and put data *) -val lookup_axclass_info = Symtab.curried_lookup o AxclassesData.get; +val lookup_info = Symtab.curried_lookup o AxclassesData.get; -fun get_axclass_info thy c = - (case lookup_axclass_info thy c of +fun get_info thy c = + (case lookup_info thy c of NONE => error ("Unknown axclass " ^ quote c) | SOME info => info); -fun put_axclass_info c info thy = - thy |> AxclassesData.put (Symtab.curried_update (c, info) (AxclassesData.get thy)); - (* class_axms *) fun class_axms thy = let val classes = Sign.classes thy in map (Thm.class_triv thy) classes @ - List.mapPartial (Option.map #intro o lookup_axclass_info thy) classes + List.mapPartial (Option.map #intro o lookup_info thy) classes end; @@ -218,7 +215,7 @@ (*declare axioms and rule*) val (axms_thy, ([intro], [axioms])) = class_thy - |> Theory.add_path bclass + |> Theory.add_path (Sign.const_of_class bclass) |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] |>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; val info = {super_classes = super_classes, intro = intro, axioms = axioms}; @@ -228,8 +225,7 @@ axms_thy |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)) |> Theory.restore_naming class_thy - |> (#1 o PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)]) - |> put_axclass_info class info; + |> AxclassesData.map (Symtab.curried_update (class, info)); in (final_thy, {intro = intro, axioms = axioms}) end; in @@ -372,9 +368,11 @@ val instanceP = OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal - ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.xname) >> (fn i => instance_subclass_proof i I) || - (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) >> (fn i => instance_arity_proof i I)) - >> (Toplevel.print oo Toplevel.theory_to_proof)); + ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.xname) + >> (fn i => instance_subclass_proof i I) || + (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) + >> (fn i => instance_arity_proof i I)) + >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.add_parsers [axclassP, instanceP];