src/HOL/Tools/Metis/metis_translate.ML

--- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -68,6 +68,7 @@
     theory -> string list -> class list -> class list * arity_clause list
   val combtyp_of : combterm -> combtyp
   val strip_combterm_comb : combterm -> combterm * combterm list
+  val combtyp_from_typ : typ -> combtyp
   val combterm_from_term :
     theory -> (string * typ) list -> term -> combterm * typ list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
@@ -393,23 +394,24 @@
         |   stripc  x =  x
     in stripc(u,[]) end
 
-fun combtype_of (Type (a, Ts)) =
-    let val (folTypes, ts) = combtypes_of Ts in
-      (CombType (`make_fixed_type_const a, folTypes), ts)
+fun combtyp_and_sorts_from_type (Type (a, Ts)) =
+    let val (tys, ts) = combtyps_and_sorts_from_types Ts in
+      (CombType (`make_fixed_type_const a, tys), ts)
     end
-  | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
-  | combtype_of (tp as TVar (x, _)) =
+  | combtyp_and_sorts_from_type (tp as TFree (a, _)) =
+    (CombTFree (`make_fixed_type_var a), [tp])
+  | combtyp_and_sorts_from_type (tp as TVar (x, _)) =
     (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
-and combtypes_of Ts =
-  let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
-    (folTyps, union_all ts)
+and combtyps_and_sorts_from_types Ts =
+  let val (tys, ts) = ListPair.unzip (map combtyp_and_sorts_from_type Ts) in
+    (tys, union_all ts)
   end
 
 (* same as above, but no gathering of sort information *)
-fun simple_combtype_of (Type (a, Ts)) =
-    CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
-  | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
-  | simple_combtype_of (TVar (x, _)) =
+fun combtyp_from_typ (Type (a, Ts)) =
+    CombType (`make_fixed_type_const a, map combtyp_from_typ Ts)
+  | combtyp_from_typ (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
+  | combtyp_from_typ (TVar (x, _)) =
     CombTVar (make_schematic_type_var x, string_of_indexname x)
 
 fun new_skolem_const_name s num_T_args =
@@ -425,37 +427,35 @@
       in (CombApp (P', Q'), union (op =) tsP tsQ) end
   | combterm_from_term thy _ (Const (c, T)) =
       let
-        val (tp, ts) = combtype_of T
+        val (tp, ts) = combtyp_and_sorts_from_type T
         val tvar_list =
           (if String.isPrefix old_skolem_const_prefix c then
              [] |> Term.add_tvarsT T |> map TVar
            else
              (c, T) |> Sign.const_typargs thy)
-          |> map simple_combtype_of
+          |> map combtyp_from_typ
         val c' = CombConst (`make_fixed_const c, tp, tvar_list)
       in  (c',ts)  end
   | combterm_from_term _ _ (Free (v, T)) =
-      let val (tp, ts) = combtype_of T
+      let val (tp, ts) = combtyp_and_sorts_from_type T
           val v' = CombConst (`make_fixed_var v, tp, [])
       in  (v',ts)  end
   | combterm_from_term _ _ (Var (v as (s, _), T)) =
     let
-      val (tp, ts) = combtype_of T
+      val (tp, ts) = combtyp_and_sorts_from_type T
       val v' =
         if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
           let
             val tys = T |> strip_type |> swap |> op ::
             val s' = new_skolem_const_name s (length tys)
-          in
-            CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
-          end
+          in CombConst (`make_fixed_const s', tp, map combtyp_from_typ tys) end
         else
           CombVar ((make_schematic_var v, string_of_indexname v), tp)
     in (v', ts) end
   | combterm_from_term _ bs (Bound j) =
       let
         val (s, T) = nth bs j
-        val (tp, ts) = combtype_of T
+        val (tp, ts) = combtyp_and_sorts_from_type T
         val v' = CombConst (`make_bound_var s, tp, [])
       in (v', ts) end
   | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"