--- a/src/Pure/Isar/element.ML Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Isar/element.ML Tue Mar 21 12:18:15 2006 +0100
@@ -342,7 +342,7 @@
val vars = Term.add_vars raw_prop [];
val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
- val fixes = rev (filter_out (equal AutoBind.thesisN o #1) frees);
+ val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees);
val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
val (prems, concl) = Logic.strip_horn prop;