src/Pure/simplifier.ML
changeset 30336 efd1bec4630a
parent 29606 fedb8be05f24
child 30356 36d0e00af606
     1.1 --- a/src/Pure/simplifier.ML	Sat Mar 07 11:32:31 2009 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sat Mar 07 11:45:56 2009 +0100
     1.3 @@ -217,14 +217,14 @@
     1.4  
     1.5  fun solve_all_tac solvers ss =
     1.6    let
     1.7 -    val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss;
     1.8 +    val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss;
     1.9      val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
    1.10    in DEPTH_SOLVE (solve_tac 1) end;
    1.11  
    1.12  (*NOTE: may instantiate unknowns that appear also in other subgoals*)
    1.13  fun generic_simp_tac safe mode ss =
    1.14    let
    1.15 -    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
    1.16 +    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss;
    1.17      val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
    1.18      val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
    1.19        (rev (if safe then solvers else unsafe_solvers)));
    1.20 @@ -238,7 +238,7 @@
    1.21  
    1.22  fun simp rew mode ss thm =
    1.23    let
    1.24 -    val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
    1.25 +    val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss;
    1.26      val tacf = solve_all_tac (rev unsafe_solvers);
    1.27      fun prover s th = Option.map #1 (Seq.pull (tacf s th));
    1.28    in rew mode prover ss thm end;