# HG changeset patch
# User blanchet
# Date 1307515663 -7200
# Node ID c0eaa8b9bff5965087de2dec8b0622623cad9506
# Parent  dd38b8ef52b9f9d1863d7488bb44b6fa52d478d7
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"

diff -r dd38b8ef52b9 -r c0eaa8b9bff5 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -57,10 +57,10 @@
     SOME ((s, _), (_, swap)) => (s, swap)
   | _ => (s, false)
 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
-    let val (s, swap) = atp_name_from_metis s in
+    let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
       ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
     end
-  | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
+  | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
 
 fun hol_term_from_metis ctxt sym_tab =
   atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
@@ -160,11 +160,14 @@
                                          " in " ^ Display.string_of_thm ctxt i_th);
                 NONE)
       fun remove_typeinst (a, t) =
-            case strip_prefix_and_unascii schematic_var_prefix a of
-                SOME b => SOME (b, t)
-              | NONE => case strip_prefix_and_unascii tvar_prefix a of
-                SOME _ => NONE          (*type instantiations are forbidden!*)
-              | NONE => SOME (a,t)    (*internal Metis var?*)
+        let val a = Metis_Name.toString a in
+          case strip_prefix_and_unascii schematic_var_prefix a of
+            SOME b => SOME (b, t)
+          | NONE =>
+            case strip_prefix_and_unascii tvar_prefix a of
+              SOME _ => NONE (* type instantiations are forbidden *)
+            | NONE => SOME (a, t) (* internal Metis var? *)
+        end
       val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
       val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
       val (vars, tms) =
@@ -349,7 +352,8 @@
       fun path_finder tm [] _ = (tm, Bound 0)
         | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
           let
-            val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix
+            val s = s |> Metis_Name.toString
+                      |> perhaps (try (strip_prefix_and_unascii const_prefix
                                        #> the #> unmangled_const_name))
           in
             if s = metis_predicator orelse s = predicator_name orelse
@@ -422,7 +426,8 @@
         in  th'  end
         handle THM _ => th;
 
-fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
+fun is_metis_literal_genuine (_, (s, _)) =
+  not (String.isPrefix class_prefix (Metis_Name.toString s))
 fun is_isabelle_literal_genuine t =
   case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
 
diff -r dd38b8ef52b9 -r c0eaa8b9bff5 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -114,14 +114,16 @@
 val prepare_helper =
   Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
 
-fun metis_name_from_atp s ary =
-  AList.lookup (op =) metis_name_table (s, ary) |> the_default (s, false)
 fun metis_term_from_atp (ATerm (s, tms)) =
   if is_tptp_variable s then
-    Metis_Term.Var s
+    Metis_Term.Var (Metis_Name.fromString s)
   else
-    let val (s, swap) = metis_name_from_atp s (length tms) in
-      Metis_Term.Fn (s, tms |> map metis_term_from_atp |> swap ? rev)
+    let
+      val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
+                      |> the_default (s, false)
+    in
+      Metis_Term.Fn (Metis_Name.fromString s,
+                     tms |> map metis_term_from_atp |> swap ? rev)
     end
 fun metis_atom_from_atp (AAtom tm) =
     (case metis_term_from_atp tm of
@@ -131,8 +133,8 @@
 fun metis_literal_from_atp (AConn (ANot, [phi])) =
     (false, metis_atom_from_atp phi)
   | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
-fun metis_literals_from_atp (AConn (AOr, [phi1, phi2])) =
-    uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2))
+fun metis_literals_from_atp (AConn (AOr, phis)) =
+    maps metis_literals_from_atp phis
   | metis_literals_from_atp phi = [metis_literal_from_atp phi]
 fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
     let
diff -r dd38b8ef52b9 -r c0eaa8b9bff5 src/Tools/Metis/make_metis
--- a/src/Tools/Metis/make_metis	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/make_metis	Wed Jun 08 08:47:43 2011 +0200
@@ -40,7 +40,6 @@
     echo -e "$FILE" >&2
     "$THIS/scripts/mlpp" -c polyml "$FILE" | \
     perl -p -e \
-'s/type name$/type name = string/;'\
 's/\bref\b/Unsynchronized.ref/g;'\
 "`grep "^\(signature\|structure\|functor\)" $FILES | \
   sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \
diff -r dd38b8ef52b9 -r c0eaa8b9bff5 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/metis.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -8262,7 +8262,7 @@
 (* A type of names.                                                          *)
 (* ------------------------------------------------------------------------- *)
 
-type name = string
+type name
 
 (* ------------------------------------------------------------------------- *)
 (* A total ordering.                                                         *)