1.1 --- a/src/Pure/simplifier.ML	Sat Jul 28 20:40:29 2007 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Sat Jul 28 20:40:30 2007 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4    val simp_del: attribute
     1.5    val cong_add: attribute
     1.6    val cong_del: attribute
     1.7 -  val get_simproc: Proof.context -> xstring -> simproc
     1.8 +  val get_simproc: Context.generic -> xstring -> simproc
     1.9    val def_simproc: {name: string, lhss: string list,
    1.10      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    1.11      local_theory -> local_theory
    1.12 @@ -109,8 +109,8 @@
    1.13  fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
    1.14  val get_simpset = ! o GlobalSimpset.get;
    1.15  
    1.16 -val change_simpset_of = change o GlobalSimpset.get;
    1.17 -fun change_simpset f = change_simpset_of (ML_Context.the_context ()) f;
    1.18 +fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f);
    1.19 +fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_context ()) f);
    1.20  
    1.21  fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
    1.22  val simpset = simpset_of o ML_Context.the_context;
    1.23 @@ -184,9 +184,9 @@
    1.24  
    1.25  (* get simprocs *)
    1.26  
    1.27 -fun get_simproc ctxt xname =
    1.28 +fun get_simproc context xname =
    1.29    let
    1.30 -    val (space, tab) = Simprocs.get (Context.Proof ctxt);
    1.31 +    val (space, tab) = Simprocs.get context;
    1.32      val name = NameSpace.intern space xname;
    1.33    in
    1.34      (case Symtab.lookup tab name of
    1.35 @@ -196,7 +196,7 @@
    1.36  
    1.37  val _ = ML_Context.value_antiq "simproc" (Scan.lift Args.name >> (fn name =>
    1.38    ("simproc",
    1.39 -    "Simplifier.get_simproc (ML_Context.the_local_context ()) " ^ ML_Syntax.print_string name)));
    1.40 +    "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name)));
    1.41  
    1.42  
    1.43  (* define simprocs *)
    1.44 @@ -220,16 +220,15 @@
    1.45         identifier = identifier}
    1.46        |> morph_simproc (LocalTheory.target_morphism lthy);
    1.47    in
    1.48 -    lthy |> LocalTheory.declaration (fn phi => fn context =>
    1.49 +    lthy |> LocalTheory.declaration (fn phi =>
    1.50        let
    1.51          val name' = Morphism.name phi name;
    1.52          val simproc' = morph_simproc phi simproc;
    1.53        in
    1.54 -        context
    1.55 -        |> Simprocs.map (fn simprocs =>
    1.56 +        Simprocs.map (fn simprocs =>
    1.57              NameSpace.extend_table naming [(name', simproc')] simprocs
    1.58                handle Symtab.DUP dup => err_dup_simproc dup)
    1.59 -        |> map_ss (fn ss => ss addsimprocs [simproc'])
    1.60 +        #> map_ss (fn ss => ss addsimprocs [simproc'])
    1.61        end)
    1.62    end;
    1.63  
    1.64 @@ -328,6 +327,27 @@
    1.65  val asm_lrN = "asm_lr";
    1.66  
    1.67  
    1.68 +(* simprocs *)
    1.69 +
    1.70 +local
    1.71 +
    1.72 +val add_del =
    1.73 +  (Args.del -- Args.colon >> K (op delsimprocs) ||
    1.74 +    Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
    1.75 +  >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
    1.76 +      (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
    1.77 +
    1.78 +in
    1.79 +
    1.80 +val simproc_att = Attrib.syntax
    1.81 +  (Scan.peek (fn context =>
    1.82 +    add_del :|-- (fn decl =>
    1.83 +      Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
    1.84 +      >> (Library.apply o map Morphism.form))));
    1.85 +
    1.86 +end;
    1.87 +  
    1.88 +
    1.89  (* conversions *)
    1.90  
    1.91  local
    1.92 @@ -351,8 +371,9 @@
    1.93  
    1.94  val _ = Context.add_setup
    1.95   (Attrib.add_attributes
    1.96 -   [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rule"),
    1.97 +   [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
    1.98      (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
    1.99 +    ("simproc", simproc_att, "declaration of simplification procedures"),
   1.100      ("simplified", simplified, "simplified rule")]);
   1.101  
   1.102  
   1.103 @@ -429,14 +450,13 @@
   1.104        else [thm RS reflect] handle THM _ => [];
   1.105  
   1.106      fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   1.107 -  in
   1.108 -    GlobalSimpset.get thy :=
   1.109 -      empty_ss setsubgoaler asm_simp_tac
   1.110 -      setSSolver safe_solver
   1.111 -      setSolver unsafe_solver
   1.112 -      setmksimps mksimps;
   1.113 -    thy
   1.114 -  end);
   1.115 +    val _ = CRITICAL (fn () =>
   1.116 +      GlobalSimpset.get thy :=
   1.117 +        empty_ss setsubgoaler asm_simp_tac
   1.118 +        setSSolver safe_solver
   1.119 +        setSolver unsafe_solver
   1.120 +        setmksimps mksimps);
   1.121 +  in thy end);
   1.122  
   1.123  end;
   1.124