tuned signature;
authorwenzelm
Thu Dec 12 17:34:50 2013 +0100 (2013-12-12)
changeset 54728445e7947c6b5
parent 54727 a806e7251cf0
child 54729 c5cd7a58cf2d
tuned signature;
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu Dec 12 16:56:53 2013 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Dec 12 17:34:50 2013 +0100
     1.3 @@ -73,10 +73,6 @@
     1.4    include BASIC_RAW_SIMPLIFIER
     1.5    exception SIMPLIFIER of string * thm
     1.6    val internal_ss: simpset ->
     1.7 -   {rules: rrule Net.net,
     1.8 -    prems: thm list,
     1.9 -    bounds: int * ((string * typ) * string) list,
    1.10 -    depth: int * bool Unsynchronized.ref} *
    1.11     {congs: (cong_name * thm) list * cong_name list,
    1.12      procs: proc Net.net,
    1.13      mk_rews:
    1.14 @@ -287,7 +283,7 @@
    1.15      loop_tacs: (string * (Proof.context -> int -> tactic)) list,
    1.16      solvers: solver list * solver list};
    1.17  
    1.18 -fun internal_ss (Simpset args) = args;
    1.19 +fun internal_ss (Simpset (_, ss2)) = ss2;
    1.20  
    1.21  fun make_ss1 (rules, prems, bounds, depth) =
    1.22    {rules = rules, prems = prems, bounds = bounds, depth = depth};
     2.1 --- a/src/Pure/simplifier.ML	Thu Dec 12 16:56:53 2013 +0100
     2.2 +++ b/src/Pure/simplifier.ML	Thu Dec 12 17:34:50 2013 +0100
     2.3 @@ -190,14 +190,14 @@
     2.4  
     2.5  fun solve_all_tac solvers ctxt =
     2.6    let
     2.7 -    val (_, {subgoal_tac, ...}) = Raw_Simplifier.internal_ss (simpset_of ctxt);
     2.8 +    val {subgoal_tac, ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
     2.9      val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt) THEN_ALL_NEW (K no_tac);
    2.10    in DEPTH_SOLVE (solve_tac 1) end;
    2.11  
    2.12  (*NOTE: may instantiate unknowns that appear also in other subgoals*)
    2.13  fun generic_simp_tac safe mode ctxt =
    2.14    let
    2.15 -    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) =
    2.16 +    val {loop_tacs, solvers = (unsafe_solvers, solvers), ...} =
    2.17        Raw_Simplifier.internal_ss (simpset_of ctxt);
    2.18      val loop_tac = FIRST' (map (fn (_, tac) => tac ctxt) (rev loop_tacs));
    2.19      val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
    2.20 @@ -212,7 +212,7 @@
    2.21  
    2.22  fun simp rew mode ctxt thm =
    2.23    let
    2.24 -    val (_, {solvers = (unsafe_solvers, _), ...}) = Raw_Simplifier.internal_ss (simpset_of ctxt);
    2.25 +    val {solvers = (unsafe_solvers, _), ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
    2.26      val tacf = solve_all_tac (rev unsafe_solvers);
    2.27      fun prover s th = Option.map #1 (Seq.pull (tacf s th));
    2.28    in rew mode prover ctxt thm end;