--- 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;