--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Sep 02 19:47:37 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Sep 02 19:53:49 2015 +0200
@@ -736,8 +736,8 @@
else Ferrante_Rackoff_Data.Nox
| _ => Ferrante_Rackoff_Data.Nox
in h end
- fun ss phi =
- simpset_of (put_simpset HOL_ss @{context} addsimps (simps phi))
+ fun ss phi ctxt =
+ simpset_of (put_simpset HOL_ss ctxt addsimps (simps phi))
in
Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"}
{isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
@@ -884,7 +884,6 @@
shows "x + t = 0 \<equiv> x = - t"
using eq_diff_eq[where a= x and b=t and c=0] by simp
-
interpretation class_dense_linordered_field: constr_dense_linorder
"op \<le>" "op <" "\<lambda>x y. 1/2 * ((x::'a::linordered_field) + y)"
by unfold_locales (dlo, dlo, auto)
@@ -1104,8 +1103,8 @@
else Ferrante_Rackoff_Data.Nox
| _ => Ferrante_Rackoff_Data.Nox
in h end;
-fun class_field_ss phi =
- simpset_of (put_simpset HOL_basic_ss @{context}
+fun class_field_ss phi ctxt =
+ simpset_of (put_simpset HOL_basic_ss ctxt
addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
|> fold Splitter.add_split [@{thm "abs_split"}, @{thm "split_max"}, @{thm "split_min"}])
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Wed Sep 02 19:47:37 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Wed Sep 02 19:53:49 2015 +0200
@@ -15,7 +15,7 @@
val funs: thm ->
{isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
whatis: morphism -> cterm -> cterm -> ord,
- simpset: morphism -> simpset} -> declaration
+ simpset: morphism -> Proof.context -> simpset} -> declaration
val match: Proof.context -> cterm -> entry option
end;
@@ -57,13 +57,15 @@
(* extra-logical functions *)
-fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data =>
- let
- val key = Morphism.thm phi raw_key;
- val _ = AList.defined eq_key data key orelse
- raise THM ("No data entry for structure key", 0, [key]);
- val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi};
- in AList.map_entry eq_key key (apsnd (K fns)) data end);
+fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi context =
+ context |> Data.map (fn data =>
+ let
+ val key = Morphism.thm phi raw_key;
+ val _ = AList.defined eq_key data key orelse
+ raise THM ("No data entry for structure key", 0, [key]);
+ val fns =
+ {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi (Context.proof_of context)};
+ in AList.map_entry eq_key key (apsnd (K fns)) data end);
fun match ctxt tm =
let