src/Pure/simplifier.ML
changeset 22717 74dbc7696083
parent 22709 9ab51bac6287
child 22770 615e19792c92
     1.1 --- a/src/Pure/simplifier.ML	Mon Apr 16 12:16:11 2007 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Mon Apr 16 16:11:03 2007 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4      val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
     1.5      val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
     1.6      val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
     1.7 -      (if safe then solvers else unsafe_solvers));
     1.8 +      (rev (if safe then solvers else unsafe_solvers)));
     1.9  
    1.10      fun simp_loop_tac i =
    1.11        Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
    1.12 @@ -286,7 +286,7 @@
    1.13  fun simp rew mode ss thm =
    1.14    let
    1.15      val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
    1.16 -    val tacf = solve_all_tac unsafe_solvers;
    1.17 +    val tacf = solve_all_tac (rev unsafe_solvers);
    1.18      fun prover s th = Option.map #1 (Seq.pull (tacf s th));
    1.19    in rew mode prover ss thm end;
    1.20