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/HOL/Tools/Metis/metis_generate.ML
changeset 46340 cac402c486b0
parent 46320 0b8b73b49848
child 46365 547d1a1dcaf6 
--- a/src/HOL/Tools/Metis/metis_generate.ML	Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Thu Jan 26 20:49:54 2012 +0100
@@ -222,10 +222,9 @@
         |> pairself (maps (map (zero_var_indexes o snd)))
     val num_conjs = length conj_clauses
     val clauses =
-      map2 (fn j => pair (Int.toString j, Local))
+      map2 (fn j => pair (Int.toString j, (Local, General)))
            (0 upto num_conjs - 1) conj_clauses @
-      (* "General" below isn't quite correct; the fact could be local. *)
-      map2 (fn j => pair (Int.toString (num_conjs + j), General))
+      map2 (fn j => pair (Int.toString (num_conjs + j), (Local, General)))
            (0 upto length fact_clauses - 1) fact_clauses
     val (old_skolems, props) =
       fold_rev (fn (name, th) => fn (old_skolems, props) =>
isabelle