Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bug fix
authorobua
Sat, 24 Sep 2005 10:47:22 +0200
changeset 17624 da9a5efecde7
parent 17623 ae4af66b3072
child 17625 1539d18e3e9f
bug fix
src/HOL/Import/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/Import/proof_kernel.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/ROOT.ML	Sat Sep 24 07:57:50 2005 +0200
+++ b/src/HOL/Import/ROOT.ML	Sat Sep 24 10:47:22 2005 +0200
@@ -3,5 +3,6 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
+proofs := 0;
 use_thy "HOL4Compat";
 use_thy "HOL4Syntax";
--- a/src/HOL/Import/proof_kernel.ML	Sat Sep 24 07:57:50 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat Sep 24 10:47:22 2005 +0200
@@ -2135,7 +2135,7 @@
 	    val thy4 = add_hol4_pending thyname thmname args thy''
 	   
 	    val sg = sign_of thy4
-	    val P' = #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4)))
+	    val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
 	    val c   =
 		let
 		    val PT = type_of P'
isabelle