# HG changeset patch
# User haftmann
# Date 1235121272 -3600
# Node ID ca058f25d3d7c1aad039e7c5e5898bd541a9bc46
# Parent  20c194b71bb7cf8c5920f7c5d6897b7074e3d537
ignore sorts in bare types

diff -r 20c194b71bb7 -r ca058f25d3d7 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Fri Feb 20 10:14:32 2009 +0100
+++ b/src/Tools/code/code_thingol.ML	Fri Feb 20 10:14:32 2009 +0100
@@ -495,9 +495,8 @@
 and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))
-and translate_typ thy algbr funcgr (TFree v_sort) =
-      translate_tyvar_sort thy algbr funcgr v_sort
-      #>> (fn (v, sort) => ITyVar v)
+and translate_typ thy algbr funcgr (TFree (v, _)) =
+      pair (ITyVar (unprefix "'" v))
   | translate_typ thy algbr funcgr (Type (tyco, tys)) =
       ensure_tyco thy algbr funcgr tyco
       ##>> fold_map (translate_typ thy algbr funcgr) tys
@@ -585,7 +584,7 @@
       #>> (fn class => Classparam (c, class));
     fun stmt_fun ((vs, raw_ty), raw_thms) =
       let
-        val ty = Logic.unvarifyT raw_ty;
+        val ty = Logic.unvarifyT raw_ty; (*FIXME change convention here*)
         val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
           then raw_thms
           else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;