# HG changeset patch
# User wenzelm
# Date 1406317443 -7200
# Node ID 5b652fd305d44798682f52eb1a3298dfb557aaaf
# Parent  e189ba8a64b984261cd75a8f4f1f224dc1b19eea
tuned comment;

diff -r e189ba8a64b9 -r 5b652fd305d4 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Jul 25 21:29:12 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Jul 25 21:44:03 2014 +0200
@@ -182,7 +182,7 @@
       val goal_concl = Logic.concl_of_goal goal 1;
       val rule_mp = hd (Logic.strip_imp_prems rule);
       val rule_concl = Logic.strip_imp_concl rule;
-      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?? *)
+      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?!? *)
       val rule_tree = combine rule_mp rule_concl;
       fun goal_tree prem = combine prem goal_concl;
       fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;