# HG changeset patch
# User berghofe
# Date 1170867638 -3600
# Node ID b89dc456dbc6522d6d661fe1d9cfab5f95c75cd9
# Parent  96a4db55a0b3e1e852855bf266bac553891e72dd
Fixed bug in mk_AbsP.

diff -r 96a4db55a0b3 -r b89dc456dbc6 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Feb 07 17:59:40 2007 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Feb 07 18:00:38 2007 +0100
@@ -308,7 +308,7 @@
 fun make_sym Ts ((x, y), prf) =
   ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
 
-fun mk_AbsP P t = AbsP ("H", P, t);
+fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
 fun elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)