1.1 --- a/src/Pure/Isar/code.ML	Mon Apr 19 07:38:35 2010 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Apr 19 11:30:08 2010 +0200
     1.3 @@ -533,17 +533,19 @@
     1.4             | THM _ => bad "Not a proper equation";
     1.5      val (rep, lhs) = dest_comb full_lhs
     1.6        handle TERM _ => bad "Not an abstract equation";
     1.7 -    val tyco = (fst o dest_Type o domain_type o snd o dest_Const) rep
     1.8 +    val (rep_const, ty) = dest_Const rep;
     1.9 +    val (tyco, sorts) = ((apsnd o map) (snd o dest_TVar) o dest_Type o domain_type) ty
    1.10        handle TERM _ => bad "Not an abstract equation";
    1.11      val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
    1.12            else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
    1.13        | NONE => ();
    1.14 -    val (_, (_, (rep', _))) = get_abstype_spec thy tyco;
    1.15 -    val rep_const = (fst o dest_Const) rep;
    1.16 +    val (vs', (_, (rep', _))) = get_abstype_spec thy tyco;
    1.17      val _ = if rep_const = rep' then ()
    1.18        else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
    1.19      val _ = check_eqn thy { allow_nonlinear = false,
    1.20        allow_consts = false, allow_pats = false } thm (lhs, rhs);
    1.21 +    val _ = if forall (Sign.subsort thy) (sorts ~~ map snd  vs') then ()
    1.22 +      else error ("Sort constraints on type arguments are weaker than in abstype certificate.")
    1.23    in (thm, tyco) end;
    1.24  
    1.25  fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
    1.26 @@ -809,7 +811,7 @@
    1.27        let
    1.28          val vs = fst (typscheme_abs thy abs_thm);
    1.29          val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
    1.30 -      in (vs, add_rhss_of_eqn thy (Thm.prop_of abs_thm) []) end;
    1.31 +      in (vs, add_rhss_of_eqn thy (map_types Logic.unvarifyT_global (Thm.prop_of concrete_thm)) []) end;
    1.32  
    1.33  fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
    1.34        let