src/HOL/Tools/record_package.ML

 
 (* access 'sel_upd' *)
 
 val get_sel_upd = #sel_upd o RecordsData.get;
 
-val get_selectors = Symtab.lookup o #selectors o get_sel_upd;
-fun is_selector sg name = is_some (get_selectors sg (Sign.intern_const sg name));
-
+val is_selector = Symtab.defined o #selectors o get_sel_upd;
 val get_updates = Symtab.lookup o #updates o get_sel_upd;
 val get_simpset = #simpset o get_sel_upd;
 
 fun put_sel_upd names simps thy =
   let

  *   X does not affect the selected subrecord.
  * - If X is a more-selector we have to make sure that S is not in the updated
  *   subrecord.
  *)
 val record_simproc =
-  Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
+  Simplifier.simproc HOL.thy "record_simp" ["s (u k r)"]   (* FIXME pattern!? *)
     (fn sg => fn ss => fn t =>
       (case t of (sel as Const (s, Type (_,[domS,rangeS])))$
                    ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
-        (case get_selectors sg s of SOME () =>
+        if is_selector sg s then
           (case get_updates sg u of SOME u_name =>
             let
               val {sel_upd={updates,...},extfields,...} = RecordsData.get sg;
 
               fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) =

                     else SOME (prove_split_simp sg ss domS
                                  (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm')))))
                | NONE => NONE)
             end
           | NONE => NONE)
-        | NONE => NONE)
+        else NONE
       | _ => NONE));
 
 (* record_upd_simproc *)
 (* simplify multiple updates:
  *  (1)  "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)"

  *    r(|more := m; A := A r|)
  * If A is contained in the fields of m we cannot remove the update A := A r!
  * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
 *)
 val record_upd_simproc =
-  Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"]
+  Simplifier.simproc HOL.thy "record_upd_simp" ["u k r"]    (* FIXME pattern *)
     (fn sg => fn ss => fn t =>
       (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
          let datatype ('a,'b) calc = Init of 'b | Inter of 'a
              val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
 

  *               record_eq_simproc       record_split_simp_tac
  * Complexity: #components * #updates     #updates
  *
  *)
 val record_eq_simproc =
-  Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
+  Simplifier.simproc HOL.thy "record_eq_simp" ["r = s"]
     (fn sg => fn _ => fn t =>
       (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
         (case rec_id (~1) T of
            "" => NONE
          | name => (case get_equalities sg name of

  * P t = 0: do not split
  * P t = ~1: completely split
  * P t > 0: split up to given bound of record extensions
  *)
 fun record_split_simproc P =
-  Simplifier.simproc (Theory.sign_of HOL.thy) "record_split_simp" ["(a t)"]
+  Simplifier.simproc HOL.thy "record_split_simp" ["a t"]
     (fn sg => fn _ => fn t =>
       (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
          if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
          then (case rec_id (~1) T of
                  "" => NONE

                       end)
          else NONE
        | _ => NONE))
 
 val record_ex_sel_eq_simproc =
-  Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
+  Simplifier.simproc HOL.thy "record_ex_sel_eq_simproc" ["Ex t"]
     (fn sg => fn ss => fn t =>
        let
          fun prove prop =
            quick_and_dirty_prove true sg [] prop
              (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
                addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
 
          fun mkeq (lr,Teq,(sel,Tsel),x) i =
-              (case get_selectors sg sel of SOME () =>
+              if is_selector sg sel then
                  let val x' = if not (loose_bvar1 (x,0))
                               then Free ("x" ^ string_of_int i, range_type Tsel)
                               else raise TERM ("",[x]);
                      val sel' = Const (sel,Tsel)$Bound 0;
                      val (l,r) = if lr then (sel',x') else (x',sel');
                   in Const ("op =",Teq)$l$r end
-               | NONE => raise TERM ("",[Const (sel,Tsel)]));
+              else raise TERM ("",[Const (sel,Tsel)]);
 
          fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) =
                            (true,Teq,(sel,Tsel),X)
            | dest_sel_eq (Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0)) =
                            (false,Teq,(sel,Tsel),X)

  * avoid problems with higher order unification.
  *)
 
 fun try_param_tac s rule i st =
   let
-    val cert = cterm_of (Thm.sign_of_thm st);
+    val cert = cterm_of (Thm.theory_of_thm st);
     val g = List.nth (prems_of st, i - 1);
     val params = Logic.strip_params g;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
     val rule' = Thm.lift_rule (st, i) rule;
     val (P, ys) = strip_comb (HOLogic.dest_Trueprop

       let val P = Free (variant variants "P", extT-->Term.propT) in
         Logic.mk_equals
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
       end;
 
-    fun prove stndrd = quick_and_dirty_prove stndrd (Theory.sign_of defs_thy);
-    val prove_standard = quick_and_dirty_prove true (Theory.sign_of defs_thy);
+    fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
+    val prove_standard = quick_and_dirty_prove true defs_thy;
     fun prove_simp stndrd simps =
       let val tac = simp_all_tac HOL_ss simps
       in fn prop => prove stndrd [] prop (K tac) end;
 
     fun inject_prf () = (prove_simp true [ext_def,abs_inject,Pair_eq] inject_prop);

         val seleqs = map mk_sel_eq all_named_vars_more
       in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end;
 
     (* 3rd stage: thms_thy *)
 
-    fun prove stndrd = quick_and_dirty_prove stndrd (Theory.sign_of defs_thy);
-    val prove_standard = quick_and_dirty_prove true (Theory.sign_of defs_thy);
+    fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
+    val prove_standard = quick_and_dirty_prove true defs_thy;
 
     fun prove_simp stndrd ss simps =
       let val tac = simp_all_tac ss simps
       in fn prop => prove stndrd [] prop (K tac) end;
 
-    val ss = get_simpset (sign_of defs_thy);
+    val ss = get_simpset defs_thy;
 
     fun sel_convs_prf () = map (prove_simp false ss
                            (sel_defs@ext_dest_convs)) sel_conv_props;
     val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
     fun sel_convs_standard_prf () = map standard sel_convs