# HG changeset patch # User wenzelm # Date 1208268733 -7200 # Node ID 750bab48223da7eed23b9f3d3d38e8a745ab7ac5 # Parent 1f711934f2217875eac371975cd2759e30bfb7b0 moved forall_elim_var(s) to more_thm.ML; get_thm(s) and hide_thms: use new table; diff -r 1f711934f221 -r 750bab48223d src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Apr 15 16:12:11 2008 +0200 +++ b/src/Pure/pure_thy.ML Tue Apr 15 16:12:13 2008 +0200 @@ -56,8 +56,6 @@ (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory val note_thmss_qualified: string -> string -> ((bstring * attribute list) * (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory - val forall_elim_var: int -> thm -> thm - val forall_elim_vars: int -> thm -> thm val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory val add_defs: bool -> ((bstring * string) * attribute list) list -> @@ -167,9 +165,6 @@ val name = NameSpace.intern (Facts.space_of facts) xname; in Option.map (pair name) (Facts.lookup (Context.Theory thy) facts name) end; -fun show_result NONE = "none" - | show_result (SOME (name, _)) = quote name; - fun get silent theory thmref = let val name = Facts.name_of_ref thmref; @@ -179,15 +174,14 @@ val _ = Theory.check_thy theory; val is_same = (case (new_res, old_res) of - (NONE, NONE) => true - | (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2) - | _ => false); + (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2) + | _ => true); val _ = if is_same orelse silent then () - else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^ - show_result new_res ^ " vs " ^ show_result old_res ^ Position.str_of pos); + else error ("Fact lookup differs from old-style thm database:\n" ^ + fst (the new_res) ^ " vs " ^ fst (the old_res) ^ Position.str_of pos); in - (case old_res of + (case new_res of NONE => error ("Unknown theorem(s) " ^ quote name ^ Position.str_of pos) | SOME (_, ths) => Facts.select thmref (map (Thm.transfer theory) ths)) end; @@ -215,12 +209,10 @@ (** store theorems **) -(* hiding -- affects current theory node only *) +(* hiding *) fun hide_thms fully names = - map_theorems (fn ((space, thms), all_facts) => - let val space' = fold (NameSpace.hide fully) names space - in ((space', thms), all_facts) end); + map_theorems (fn (theorems, all_facts) => (theorems, fold (Facts.hide fully) names all_facts)); (* fact specifications *) @@ -333,32 +325,11 @@ ||> Sign.restore_naming thy; -(* forall_elim_var(s) -- belongs to drule.ML *) - -fun forall_elim_vars_aux strip_vars i th = - let - val thy = Thm.theory_of_thm th; - val {tpairs, prop, ...} = Thm.rep_thm th; - val add_used = Term.fold_aterms - (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I); - val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []); - val vars = strip_vars prop; - val cvars = (Name.variant_list used (map #1 vars), vars) - |> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T))); - in fold Thm.forall_elim cvars th end; - -val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars; - -fun forall_elim_var i th = forall_elim_vars_aux - (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)] - | _ => raise THM ("forall_elim_vars", i, [th])) i th; - - (* store axioms as theorems *) local fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name); - fun get_axs thy named_axs = map (forall_elim_vars 0 o get_ax thy) named_axs; + fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs; fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy => let val named_ax = [(name, ax)];