diff -r 6dd60d1191bf -r 8f9dea697b8d src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Tue Oct 09 19:48:55 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Wed Oct 10 10:50:11 2007 +0200
@@ -101,8 +101,8 @@
   fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
     | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
 
-  fun default_sort ctxt (ResClause.FOLTVar _, _) = false
-    | default_sort ctxt (ResClause.FOLTFree x, ss) = (ss = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
+  fun default_sort ctxt (TVar _) = false
+    | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
 
   fun metis_of_tfree tf = 
     Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
@@ -503,7 +503,7 @@
 
   (*Extract TFree constraints from context to include as conjecture clauses*)
   fun init_tfrees ctxt =
-    let fun add ((a,i),s) ys = if i = ~1 then (ResClause.FOLTFree a,s) :: ys else ys
+    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
     in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
 
   (*transform isabelle clause to metis clause *)