# HG changeset patch
# User blanchet
# Date 1371157100 14400
# Node ID ddb16589b711ec52828010bec5d86038bde88350
# Parent  a231e6f897379256266fddbb6c1b37ee14116cea
tuning

diff -r a231e6f89737 -r ddb16589b711 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jun 13 14:35:05 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jun 13 16:58:20 2013 -0400
@@ -5,7 +5,7 @@
 Isar proof reconstruction from ATP proofs.
 *)
 
-signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
+signature SLEDGEHAMMER_RECONSTRUCT =
 sig
   type 'a proof = 'a ATP_Proof.proof
   type stature = ATP_Problem_Generate.stature
@@ -45,7 +45,7 @@
     -> string
 end;
 
-structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
+structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
 struct
 
 open ATP_Util