# HG changeset patch
# User haftmann
# Date 1403986401 -7200
# Node ID 4aef934d43ad3d63a622759e4bf97f9165179847
# Parent  47c8475e7864d048c55871b31f68fe21f7e35688
tuned interface

diff -r 47c8475e7864 -r 4aef934d43ad src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Jun 28 22:13:20 2014 +0200
+++ b/src/Pure/Isar/code.ML	Sat Jun 28 22:13:21 2014 +0200
@@ -66,8 +66,8 @@
   val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
   val is_constr: theory -> string -> bool
   val is_abstr: theory -> string -> bool
-  val get_cert: theory -> { functrans: ((thm * bool) list -> (thm * bool) list option) list,
-    ss: simpset } -> string -> cert
+  val get_cert: Proof.context -> ((thm * bool) list -> (thm * bool) list option) list
+    -> string -> cert
   val get_case_scheme: theory -> string -> (int * (int * string option list)) option
   val get_case_cong: theory -> string -> thm option
   val undefineds: theory -> string list
@@ -922,9 +922,9 @@
   #> (map o apfst) (preprocess eqn_conv ctxt)
   #> cert_of_eqns ctxt c;
 
-fun get_cert thy { functrans, ss } c =
+fun get_cert ctxt functrans c =
   let
-    val ctxt = thy |> Proof_Context.init_global |> put_simpset ss;
+    val thy = Proof_Context.theory_of ctxt;
   in
     case retrieve_raw thy c of
       Default (_, eqns_lazy) => Lazy.force eqns_lazy
diff -r 47c8475e7864 -r 4aef934d43ad src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sat Jun 28 22:13:20 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sat Jun 28 22:13:21 2014 +0200
@@ -321,7 +321,7 @@
         val thy = Proof_Context.theory_of ctxt;
         val functrans = (map (fn (_, (_, f)) => f ctxt)
           o #functrans o the_thmproc) thy;
-        val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
+        val cert = Code.get_cert ctxt functrans c;
         val (lhs, rhss) =
           Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;