Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/recon_reconstruct_proof.ML
changeset 15684 5ec4d21889d6
parent 15642 028059faa963 
--- a/src/HOL/Tools/ATP/recon_reconstruct_proof.ML	Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_reconstruct_proof.ML	Fri Apr 08 18:43:39 2005 +0200
@@ -53,7 +53,7 @@
                             val prems = prems_of th
                             val fac1 = get_nth (lit1+1) prems
                             val fac2 = get_nth (lit2+1) prems
-                            val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
+                            val unif_env = unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
                             val newenv = getnewenv unif_env
                             val envlist = alist_of newenv
                             
@@ -140,7 +140,7 @@
 
                            (* get bit of th2 to unify with lhs of th1 *)
                             val unif_lit = get_unif_lit (dest_Trueprop fac2) lhs
-                            val unif_env = unifiers (Mainsign,myenv, [(unif_lit, lhs)])
+                            val unif_env = unifiers (Mainsign,Envir.empty 0, [(unif_lit, lhs)])
                             val newenv = getnewenv unif_env
                             val envlist = alist_of newenv
                             val newsubsts = mksubstlist envlist []
@@ -296,10 +296,6 @@
 
 fun second_pair (a,b,c) = (b,c);
 
-fun one_of_three (a,b,c) = a;
-fun two_of_three (a,b,c) = b;
-fun three_of_three (a,b,c) = c;
-
 (*************************)
 (* reconstruct res proof *)
 (*************************)
isabelle