# HG changeset patch
# User wenzelm
# Date 1441216429 -7200
# Node ID 969eb24297afe766d01849fdb26ce903526a5526
# Parent  66225f7dd314c8bf9785340ea08c0f0294e25881
clarified context;

diff -r 66225f7dd314 -r 969eb24297af src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- 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"}])
 
diff -r 66225f7dd314 -r 969eb24297af src/HOL/Decision_Procs/ferrante_rackoff_data.ML
--- 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