changeset 22568 | ed7aa5a350ef |
parent 21745 | a1d8806b5267 |
child 22900 | f8a7c10e1bd0 |
--- a/src/Pure/Isar/rule_cases.ML Tue Apr 03 19:24:11 2007 +0200 +++ b/src/Pure/Isar/rule_cases.ML Tue Apr 03 19:24:13 2007 +0200 @@ -330,7 +330,7 @@ | mutual_rule _ [th] = SOME ([0], th) | mutual_rule ctxt (ths as th :: _) = let - val ((_, ths'), ctxt') = Variable.import true ths ctxt; + val ((_, ths'), ctxt') = Variable.import_thms true ths ctxt; val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths'; val (ns, rls) = split_list (map #2 rules); in