# HG changeset patch
# User paulson
# Date 916225698 -3600
# Node ID b321f5aaa5f42888e405022e41082447fb57e33e
# Parent  5e4871c5136b52978116788c6f279f71dcbc0a18
generalized qed_spec_mp code to work for ZF

diff -r 5e4871c5136b -r b321f5aaa5f4 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Wed Jan 13 11:57:09 1999 +0100
+++ b/src/FOL/IFOL.ML	Wed Jan 13 12:08:18 1999 +0100
@@ -6,9 +6,6 @@
 Tactics and lemmas for IFOL.thy (intuitionistic first-order logic)
 *)
 
-open IFOL;
-
-
 qed_goalw "TrueI" IFOL.thy [True_def] "True"
  (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]);
 
@@ -242,7 +239,8 @@
 val prems = goal IFOL.thy "(A == B) ==> A = B";
 by (rewrite_goals_tac prems);
 by (rtac refl 1);
-qed "def_imp_eq";
+qed "meta_eq_to_obj_eq";
+
 
 (*Substitution: rule and tactic*)
 bind_thm ("ssubst", sym RS subst);
@@ -250,7 +248,7 @@
 (*Apply an equality or definition ONCE.
   Fails unless the substitution has an effect*)
 fun stac th = 
-  let val th' = th RS def_imp_eq handle _ => th
+  let val th' = th RS meta_eq_to_obj_eq handle _ => th
   in  CHANGED_GOAL (rtac (th' RS ssubst))
   end;
 
@@ -397,21 +395,25 @@
 
 (** strip ALL and --> from proved goal while preserving ALL-bound var names **)
 
+fun make_new_spec rl =
+  (* Use a crazy name to avoid forall_intr failing because of
+     duplicate variable name *)
+  let val myspec = read_instantiate [("P","?wlzickd")] rl
+      val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
+      val cvx = cterm_of (#sign(rep_thm myspec)) vx
+  in (vxT, forall_intr cvx myspec) end;
+
 local
 
-(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
-val myspec = read_instantiate [("P","?XXX")] spec;
-val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
-val cvx = cterm_of (#sign(rep_thm myspec)) vx;
-val aspec = forall_intr cvx myspec;
+val (specT,  spec')  = make_new_spec spec
 
 in
 
 fun RSspec th =
   (case concl_of th of
      _ $ (Const("All",_) $ Abs(a,_,_)) =>
-         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
-         in th RS forall_elim ca aspec end
+         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT))
+         in th RS forall_elim ca spec' end
   | _ => raise THM("RSspec",0,[th]));
 
 fun RSmp th =
@@ -420,9 +422,9 @@
   | _ => raise THM("RSmp",0,[th]));
 
 fun normalize_thm funs =
-let fun trans [] th = th
-      | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
-in trans funs end;
+  let fun trans [] th = th
+	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
+  in trans funs end;
 
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())