# HG changeset patch
# User smolkas
# Date 1369219147 -7200
# Node ID 39ac12f31f5cdb9cdb2582680b146611991a3be1
# Parent  06db08182c4bb59bc6203924529c938a033a313e
tuned

diff -r 06db08182c4b -r 39ac12f31f5c src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed May 22 08:46:39 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed May 22 12:39:07 2013 +0200
@@ -9,7 +9,7 @@
 signature SLEDGEHAMMER_PROOF =
 sig
   type label = string * int
-  type facts = label list * string list
+  type facts = label list * string list (* local & global *)
 
   datatype isar_qualifier = Show | Then
 
@@ -68,8 +68,6 @@
 fun fix_of_proof (Proof (fix, _, _)) = fix
 fun assms_of_proof (Proof (_, assms, _)) = assms
 fun steps_of_proof (Proof (_, _, steps)) = steps
-(*fun map_steps_of_proof f (Proof (fix, assms, steps)) =
-  Proof(fix, assms, f steps)*)
 
 fun label_of_step (Obtain (_, _, l, _, _)) = SOME l
   | label_of_step (Prove (_, l, _, _)) = SOME l