--- a/src/Pure/Isar/calculation.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Dec 16 16:31:36 2015 +0100
@@ -85,12 +85,13 @@
(* symmetric *)
-val symmetric = Thm.rule_attribute (fn context => fn th =>
- (case Seq.chop 2
- (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
- ([th'], _) => Drule.zero_var_indexes th'
- | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
- | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
+val symmetric =
+ Thm.rule_attribute [] (fn context => fn th =>
+ (case Seq.chop 2
+ (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
+ ([th'], _) => Drule.zero_var_indexes th'
+ | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
+ | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
(* concrete syntax *)