1.1 --- a/src/Pure/Proof/proofchecker.ML	Tue Jun 01 10:48:38 2010 +0200
     1.2 +++ b/src/Pure/Proof/proofchecker.ML	Tue Jun 01 10:53:55 2010 +0200
     1.3 @@ -28,6 +28,48 @@
     1.4  val beta_eta_convert =
     1.5    Conv.fconv_rule Drule.beta_eta_conversion;
     1.6  
     1.7 +(* equality modulo renaming of type variables *)
     1.8 +fun is_equal t t' =
     1.9 +  let
    1.10 +    val atoms = fold_types (fold_atyps (insert (op =))) t [];
    1.11 +    val atoms' = fold_types (fold_atyps (insert (op =))) t' []
    1.12 +  in
    1.13 +    length atoms = length atoms' andalso
    1.14 +    map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
    1.15 +  end;
    1.16 +
    1.17 +fun pretty_prf thy vs Hs prf =
    1.18 +  let val prf' = prf |> prf_subst_bounds (map Free vs) |>
    1.19 +    prf_subst_pbounds (map (Hyp o prop_of) Hs)
    1.20 +  in
    1.21 +    (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
    1.22 +     Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
    1.23 +  end;
    1.24 +
    1.25 +fun pretty_term thy vs _ t =
    1.26 +  let val t' = subst_bounds (map Free vs, t)
    1.27 +  in
    1.28 +    (Syntax.pretty_term_global thy t',
    1.29 +     Syntax.pretty_typ_global thy (fastype_of t'))
    1.30 +  end;
    1.31 +
    1.32 +fun appl_error thy prt vs Hs s f a =
    1.33 +  let
    1.34 +    val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
    1.35 +    val (pp_a, pp_aT) = prt thy vs Hs a
    1.36 +  in
    1.37 +    error (cat_lines
    1.38 +      [s,
    1.39 +       "",
    1.40 +       Pretty.string_of (Pretty.block
    1.41 +         [Pretty.str "Operator:", Pretty.brk 2, pp_f,
    1.42 +           Pretty.str " ::", Pretty.brk 1, pp_fT]),
    1.43 +       Pretty.string_of (Pretty.block
    1.44 +         [Pretty.str "Operand:", Pretty.brk 3, pp_a,
    1.45 +           Pretty.str " ::", Pretty.brk 1, pp_aT]),
    1.46 +       ""])
    1.47 +  end;
    1.48 +
    1.49  fun thm_of_proof thy prf =
    1.50    let
    1.51      val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
    1.52 @@ -45,9 +87,9 @@
    1.53  
    1.54      fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
    1.55            let
    1.56 -            val thm = Drule.implies_intr_hyps (lookup name);
    1.57 +            val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
    1.58              val {prop, ...} = rep_thm thm;
    1.59 -            val _ = if prop aconv prop' then () else
    1.60 +            val _ = if is_equal prop prop' then () else
    1.61                error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    1.62                  Syntax.string_of_term_global thy prop ^ "\n\n" ^
    1.63                  Syntax.string_of_term_global thy prop');
    1.64 @@ -70,7 +112,10 @@
    1.65            let
    1.66              val thm = thm_of (vs, names) Hs prf;
    1.67              val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
    1.68 -          in Thm.forall_elim ct thm end
    1.69 +          in
    1.70 +            Thm.forall_elim ct thm
    1.71 +            handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
    1.72 +          end
    1.73  
    1.74        | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
    1.75            let
    1.76 @@ -86,6 +131,7 @@
    1.77              val thm' = beta_eta_convert (thm_of vars Hs prf');
    1.78            in
    1.79              Thm.implies_elim thm thm'
    1.80 +            handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
    1.81            end
    1.82  
    1.83        | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)