Thm.prop_of;

--- a/src/Pure/Isar/calculation.ML	Thu Jan 17 21:04:36 2002 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Jan 17 21:04:48 2002 +0100
@@ -156,7 +156,7 @@
 
 fun calculate final opt_rules print state =
   let
-    val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
+    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
 

--- a/src/Pure/Isar/context_rules.ML	Thu Jan 17 21:04:36 2002 +0100
+++ b/src/Pure/Isar/context_rules.ML	Thu Jan 17 21:04:48 2002 +0100
@@ -182,7 +182,7 @@
   map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
 
 fun find_erules _ [] = K []
-  | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
+  | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact));
 fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
 
 fun find_rules_netpair weighted facts goal (inet, enet) =

--- a/src/Pure/Isar/isar_output.ML	Thu Jan 17 21:04:36 2002 +0100
+++ b/src/Pure/Isar/isar_output.ML	Thu Jan 17 21:04:48 2002 +0100
@@ -295,7 +295,7 @@
 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
 
 fun pretty_thms ctxt thms =
-  Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
+  Pretty.chunks (map (pretty_term ctxt o Thm.prop_of) thms);
 
 fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
   Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);