src/Pure/Isar/calculation.ML
changeset 19861 620d90091788
parent 19074 77580f732e37
child 20898 113c9516a2d7
     1.1 --- a/src/Pure/Isar/calculation.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4  (* symmetric *)
     1.5  
     1.6  val symmetric = Thm.rule_attribute (fn x => fn th =>
     1.7 -  (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
     1.8 +  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
     1.9      ([th'], _) => th'
    1.10    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    1.11    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));