# HG changeset patch
# User smolkas
# Date 1373542399 -7200
# Node ID 02713cd2c2cd32840b49c822bd72e193b7bdd813
# Parent  d28d2d89034d46ad15080ed61b61305143e28500
tuned

diff -r d28d2d89034d -r 02713cd2c2cd src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 11 11:40:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 11 13:33:19 2013 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_print.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
 
diff -r d28d2d89034d -r 02713cd2c2cd src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jul 11 11:40:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jul 11 13:33:19 2013 +0200
@@ -20,8 +20,8 @@
     Proof of fix * assms * isar_step list
   and isar_step =
     Let of term * term |
-  (* for |fix|>0, this is an obtain step; step may contain subproofs *)
-  Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
+    (* for |fix|>0, this is an obtain step; step may contain subproofs *)
+    Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
   and byline =
     By_Metis of facts
 
diff -r d28d2d89034d -r 02713cd2c2cd src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jul 11 11:40:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jul 11 13:33:19 2013 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen