# HG changeset patch
# User wenzelm
# Date 1011297888 -3600
# Node ID 3be853cf19cf1b30e818699bc037bcef794a6ead
# Parent  163a85ba885b0bc58281920aff0816f8b553c937
Thm.prop_of;

diff -r 163a85ba885b -r 3be853cf19cf src/Pure/Isar/calculation.ML
--- 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;
 
diff -r 163a85ba885b -r 3be853cf19cf src/Pure/Isar/context_rules.ML
--- 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) =
diff -r 163a85ba885b -r 3be853cf19cf src/Pure/Isar/isar_output.ML
--- 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);