--- 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;