--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Mar 04 19:53:18 2015 +0100
@@ -31,7 +31,7 @@
let
val ((_, intros'), ctxt') = Variable.importT intros ctxt
val pred' =
- fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
+ fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (Thm.prop_of (hd intros')))))
val Ts = binder_types (fastype_of pred')
val argTs = map fastype_of args
val Tsubst = Type.raw_matches (argTs, Ts) Vartab.empty
@@ -61,8 +61,8 @@
fun specialise_intros black_list (pred, intros) pats thy =
let
val ctxt = Proof_Context.init_global thy
- val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
- val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
+ val maxidx = fold (Term.maxidx_term o Thm.prop_of) intros ~1
+ val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
val result_pats = map Var (fold_rev Term.add_vars pats [])
fun mk_fresh_name names =
@@ -82,7 +82,7 @@
val specialised_const = Const (constname, constT)
fun specialise_intro intro =
(let
- val (prems, concl) = Logic.strip_horn (prop_of intro)
+ val (prems, concl) = Logic.strip_horn (Thm.prop_of intro)
val env = Pattern.unify (Context.Theory thy)
(HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0)
val prems = map (Envir.norm_term env) prems
@@ -201,7 +201,7 @@
let
(* FIXME: only necessary because of sloppy Logic.unvarify in restrict_pattern *)
val intros = Drule.zero_var_indexes_list intros
- val (intros_t', thy') = (fold_map o fold_map_atoms) detect' (map prop_of intros) thy
+ val (intros_t', thy') = (fold_map o fold_map_atoms) detect' (map Thm.prop_of intros) thy
in
((constname, map (Skip_Proof.make_thm thy') intros_t'), thy')
end