Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/rule_cases.ML
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
isabelle