1.1 --- a/src/Pure/Isar/code_unit.ML	Fri Feb 20 18:29:09 2009 +0100
     1.2 +++ b/src/Pure/Isar/code_unit.ML	Fri Feb 20 18:29:10 2009 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4    val constrset_of_consts: theory -> (string * typ) list
     1.5      -> string * ((string * sort) list * (string * typ list) list)
     1.6  
     1.7 -  (*defining equations*)
     1.8 +  (*code equations*)
     1.9    val assert_eqn: theory -> thm -> thm
    1.10    val mk_eqn: theory -> thm -> thm * bool
    1.11    val assert_linear: (string -> bool) -> thm * bool -> thm * bool
    1.12 @@ -76,10 +76,11 @@
    1.13  
    1.14  fun typscheme thy (c, ty) =
    1.15    let
    1.16 -    fun dest (TVar ((v, 0), sort)) = (v, sort)
    1.17 +    val ty' = Logic.unvarifyT ty;
    1.18 +    fun dest (TFree (v, sort)) = (v, sort)
    1.19        | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty);
    1.20 -    val vs = map dest (Sign.const_typargs thy (c, ty));
    1.21 -  in (vs, ty) end;
    1.22 +    val vs = map dest (Sign.const_typargs thy (c, ty'));
    1.23 +  in (vs, Type.strip_sorts ty') end;
    1.24  
    1.25  fun inst_thm thy tvars' thm =
    1.26    let
    1.27 @@ -313,10 +314,10 @@
    1.28      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
    1.29      val vs = Name.names Name.context Name.aT sorts;
    1.30      val cs''' = map (inst vs) cs'';
    1.31 -  in (tyco, (vs, cs''')) end;
    1.32 +  in (tyco, (vs, rev cs''')) end;
    1.33  
    1.34  
    1.35 -(* defining equations *)
    1.36 +(* code equations *)
    1.37  
    1.38  fun assert_eqn thy thm =
    1.39    let
    1.40 @@ -351,7 +352,7 @@
    1.41              ^ Display.string_of_thm thm)
    1.42        | check 0 (Var _) = ()
    1.43        | check _ (Var _) = bad_thm
    1.44 -          ("Variable with application on left hand side of defining equation\n"
    1.45 +          ("Variable with application on left hand side of code equation\n"
    1.46              ^ Display.string_of_thm thm)
    1.47        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
    1.48        | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
    1.49 @@ -363,7 +364,7 @@
    1.50      val ty_decl = Sign.the_const_type thy c;
    1.51      val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
    1.52        then () else bad_thm ("Type\n" ^ string_of_typ thy ty
    1.53 -           ^ "\nof defining equation\n"
    1.54 +           ^ "\nof code equation\n"
    1.55             ^ Display.string_of_thm thm
    1.56             ^ "\nis incompatible with declared function type\n"
    1.57             ^ string_of_typ thy ty_decl)
    1.58 @@ -388,7 +389,7 @@
    1.59  fun assert_linear is_cons (thm, false) = (thm, false)
    1.60    | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true)
    1.61        else bad_thm
    1.62 -        ("Duplicate variables on left hand side of defining equation:\n"
    1.63 +        ("Duplicate variables on left hand side of code equation:\n"
    1.64            ^ Display.string_of_thm thm);
    1.65  
    1.66  

     2.1 --- a/src/Tools/nbe.ML	Fri Feb 20 18:29:09 2009 +0100
     2.2 +++ b/src/Tools/nbe.ML	Fri Feb 20 18:29:10 2009 +0100
     2.3 @@ -389,8 +389,8 @@
     2.4              val ts' = take_until is_dict ts;
     2.5              val c = const_of_idx idx;
     2.6              val (_, T) = Code.default_typscheme thy c;
     2.7 -            val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
     2.8 -            val typidx' = typidx + maxidx_of_typ T' + 1;
     2.9 +            val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T;
    2.10 +            val typidx' = typidx + 1;
    2.11            in of_apps bounds (Term.Const (c, T'), ts') typidx' end
    2.12        | of_univ bounds (Free (name, ts)) typidx =
    2.13            of_apps bounds (Term.Free (name, dummyT), ts) typidx