author | wenzelm |
Tue, 08 Dec 2015 11:28:57 +0100 | |
changeset 61812 | 71446a608dfd |
parent 61811 | 1530a0f19539 |
child 61813 | b84688dd7f6b |
--- a/src/Pure/Isar/method.ML Tue Dec 08 10:49:08 2015 +0100 +++ b/src/Pure/Isar/method.ML Tue Dec 08 11:28:57 2015 +0100 @@ -694,7 +694,7 @@ setup @{binding "-"} (Scan.succeed (K insert_facts)) "insert current facts, nothing else" #> setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt => - METHOD_CASES (fn facts => fn st => + METHOD_CASES (fn _ => fn st => let val _ = (case drop (Thm.nprems_of st) names of