# HG changeset patch
# User obua
# Date 1127551642 -7200
# Node ID da9a5efecde74f1524c5752ad58efc2cca2ed480
# Parent  ae4af66b30720b6849ab329e3fd7890f4c4d839f
bug fix

diff -r ae4af66b3072 -r da9a5efecde7 src/HOL/Import/ROOT.ML
--- 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";
diff -r ae4af66b3072 -r da9a5efecde7 src/HOL/Import/proof_kernel.ML
--- 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'