1.1 --- a/src/Pure/pure_thy.ML	Tue Apr 15 16:12:11 2008 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Apr 15 16:12:13 2008 +0200
     1.3 @@ -56,8 +56,6 @@
     1.4      (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
     1.5    val note_thmss_qualified: string -> string -> ((bstring * attribute list) *
     1.6      (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
     1.7 -  val forall_elim_var: int -> thm -> thm
     1.8 -  val forall_elim_vars: int -> thm -> thm
     1.9    val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
    1.10    val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
    1.11    val add_defs: bool -> ((bstring * string) * attribute list) list ->
    1.12 @@ -167,9 +165,6 @@
    1.13      val name = NameSpace.intern (Facts.space_of facts) xname;
    1.14    in Option.map (pair name) (Facts.lookup (Context.Theory thy) facts name) end;
    1.15  
    1.16 -fun show_result NONE = "none"
    1.17 -  | show_result (SOME (name, _)) = quote name;
    1.18 -
    1.19  fun get silent theory thmref =
    1.20    let
    1.21      val name = Facts.name_of_ref thmref;
    1.22 @@ -179,15 +174,14 @@
    1.23      val _ = Theory.check_thy theory;
    1.24      val is_same =
    1.25        (case (new_res, old_res) of
    1.26 -        (NONE, NONE) => true
    1.27 -      | (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2)
    1.28 -      | _ => false);
    1.29 +        (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2)
    1.30 +      | _ => true);
    1.31      val _ =
    1.32        if is_same orelse silent then ()
    1.33 -      else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
    1.34 -        show_result new_res ^ " vs " ^ show_result old_res ^ Position.str_of pos);
    1.35 +      else error ("Fact lookup differs from old-style thm database:\n" ^
    1.36 +        fst (the new_res) ^ " vs " ^ fst (the old_res) ^ Position.str_of pos);
    1.37    in
    1.38 -    (case old_res of
    1.39 +    (case new_res of
    1.40        NONE => error ("Unknown theorem(s) " ^ quote name ^ Position.str_of pos)
    1.41      | SOME (_, ths) => Facts.select thmref (map (Thm.transfer theory) ths))
    1.42    end;
    1.43 @@ -215,12 +209,10 @@
    1.44  
    1.45  (** store theorems **)
    1.46  
    1.47 -(* hiding -- affects current theory node only *)
    1.48 +(* hiding *)
    1.49  
    1.50  fun hide_thms fully names =
    1.51 -  map_theorems (fn ((space, thms), all_facts) =>
    1.52 -    let val space' = fold (NameSpace.hide fully) names space
    1.53 -    in ((space', thms), all_facts) end);
    1.54 +  map_theorems (fn (theorems, all_facts) => (theorems, fold (Facts.hide fully) names all_facts));
    1.55  
    1.56  
    1.57  (* fact specifications *)
    1.58 @@ -333,32 +325,11 @@
    1.59    ||> Sign.restore_naming thy;
    1.60  
    1.61  
    1.62 -(* forall_elim_var(s) -- belongs to drule.ML *)
    1.63 -
    1.64 -fun forall_elim_vars_aux strip_vars i th =
    1.65 -  let
    1.66 -    val thy = Thm.theory_of_thm th;
    1.67 -    val {tpairs, prop, ...} = Thm.rep_thm th;
    1.68 -    val add_used = Term.fold_aterms
    1.69 -      (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I);
    1.70 -    val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
    1.71 -    val vars = strip_vars prop;
    1.72 -    val cvars = (Name.variant_list used (map #1 vars), vars)
    1.73 -      |> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T)));
    1.74 -  in fold Thm.forall_elim cvars th end;
    1.75 -
    1.76 -val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars;
    1.77 -
    1.78 -fun forall_elim_var i th = forall_elim_vars_aux
    1.79 -  (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
    1.80 -  | _ => raise THM ("forall_elim_vars", i, [th])) i th;
    1.81 -
    1.82 -
    1.83  (* store axioms as theorems *)
    1.84  
    1.85  local
    1.86    fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name);
    1.87 -  fun get_axs thy named_axs = map (forall_elim_vars 0 o get_ax thy) named_axs;
    1.88 +  fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
    1.89    fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
    1.90      let
    1.91        val named_ax = [(name, ax)];