src/Pure/Isar/rule_cases.ML

 
 fun mutual_rule _ [] = NONE
   | 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 true ths ctxt;
         val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
         val (ns, rls) = split_list (map #2 rules);
       in
         if not (forall (equal_cterms prems o #1) rules) then NONE
         else