1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Nov 26 18:07:00 2010 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Nov 26 22:33:21 2010 +0100
     1.3 @@ -573,12 +573,12 @@
     1.4  
     1.5  fun ensure_tyco thy algbr eqngr permissive tyco =
     1.6    let
     1.7 -    val (vs, cos) = Code.get_type thy tyco;
     1.8 +    val ((vs, cos), _) = Code.get_type thy tyco;
     1.9      val stmt_datatype =
    1.10        fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    1.11 -      ##>> fold_map (fn ((c, vs), tys) =>
    1.12 +      ##>> fold_map (fn (c, (vs, tys)) =>
    1.13          ensure_const thy algbr eqngr permissive c
    1.14 -        ##>> pair (map (unprefix "'") vs)
    1.15 +        ##>> pair (map (unprefix "'" o fst) vs)
    1.16          ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
    1.17        #>> (fn info => Datatype (tyco, info));
    1.18    in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end