1.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Thu Jan 26 20:49:54 2012 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Thu Jan 26 20:49:54 2012 +0100
     1.3 @@ -222,10 +222,9 @@
     1.4          |> pairself (maps (map (zero_var_indexes o snd)))
     1.5      val num_conjs = length conj_clauses
     1.6      val clauses =
     1.7 -      map2 (fn j => pair (Int.toString j, Local))
     1.8 +      map2 (fn j => pair (Int.toString j, (Local, General)))
     1.9             (0 upto num_conjs - 1) conj_clauses @
    1.10 -      (* "General" below isn't quite correct; the fact could be local. *)
    1.11 -      map2 (fn j => pair (Int.toString (num_conjs + j), General))
    1.12 +      map2 (fn j => pair (Int.toString (num_conjs + j), (Local, General)))
    1.13             (0 upto length fact_clauses - 1) fact_clauses
    1.14      val (old_skolems, props) =
    1.15        fold_rev (fn (name, th) => fn (old_skolems, props) =>