--- a/src/HOL/Tools/Function/function_elims.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML Wed Mar 04 19:53:18 2015 +0100
@@ -43,7 +43,7 @@
if Logic.occs (Free x, t) then raise Match else false
| _ => raise Match);
fun mk_eq thm =
- (if inspect (prop_of thm) then [thm RS eq_reflection]
+ (if inspect (Thm.prop_of thm) then [thm RS eq_reflection]
else [Thm.symmetric (thm RS eq_reflection)])
handle Match => [];
val simpset =
@@ -80,7 +80,7 @@
fun mk_partial_elim_rules ctxt result =
let
val thy = Proof_Context.theory_of ctxt;
- val cert = cterm_of thy;
+ val cert = Thm.cterm_of thy;
val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
val n_fs = length fs;
@@ -98,14 +98,14 @@
val f_simps =
filter (fn r =>
- (prop_of r |> Logic.strip_assums_concl
+ (Thm.prop_of r |> Logic.strip_assums_concl
|> HOLogic.dest_Trueprop
|> dest_funprop |> fst |> fst) = f)
psimps;
val arity =
hd f_simps
- |> prop_of
+ |> Thm.prop_of
|> Logic.strip_assums_concl
|> HOLogic.dest_Trueprop
|> snd o fst o dest_funprop