src/Pure/raw_simplifier.ML
changeset 55000 782b8cc9233d
parent 54997 811c35e81ac5
child 55014 a93f496f6c30
     1.1 --- a/src/Pure/raw_simplifier.ML	Sun Jan 12 16:42:02 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sun Jan 12 18:34:00 2014 +0100
     1.3 @@ -114,7 +114,6 @@
     1.4    val simp_trace_raw: Config.raw
     1.5    val simp_debug_raw: Config.raw
     1.6    val add_prems: thm list -> Proof.context -> Proof.context
     1.7 -  val debug_bounds: bool Unsynchronized.ref
     1.8    val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
     1.9      Proof.context -> Proof.context
    1.10    val set_solvers: solver list -> Proof.context -> Proof.context
    1.11 @@ -317,14 +316,16 @@
    1.12  
    1.13  (* empty *)
    1.14  
    1.15 -fun init_ss mk_rews termless subgoal_tac solvers =
    1.16 -  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false)),
    1.17 +fun init_ss bounds depth mk_rews termless subgoal_tac solvers =
    1.18 +  make_simpset ((Net.empty, [], bounds, depth),
    1.19      (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
    1.20  
    1.21  fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
    1.22  
    1.23  val empty_ss =
    1.24    init_ss
    1.25 +    (0, [])
    1.26 +    (0, Unsynchronized.ref false)
    1.27      {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
    1.28        mk_cong = K I,
    1.29        mk_sym = default_mk_sym,
    1.30 @@ -398,8 +399,8 @@
    1.31  fun map_ss f = Context.mapping (map_theory_simpset f) f;
    1.32  
    1.33  val clear_simpset =
    1.34 -  map_simpset (fn Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
    1.35 -    init_ss mk_rews termless subgoal_tac solvers);
    1.36 +  map_simpset (fn Simpset ({bounds, depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
    1.37 +    init_ss bounds depth mk_rews termless subgoal_tac solvers);
    1.38  
    1.39  
    1.40  (* simp depth *)
    1.41 @@ -1321,27 +1322,6 @@
    1.42      prover: how to solve premises in conditional rewrites and congruences
    1.43  *)
    1.44  
    1.45 -val debug_bounds = Unsynchronized.ref false;
    1.46 -
    1.47 -fun check_bounds ctxt ct =
    1.48 -  if ! debug_bounds then
    1.49 -    let
    1.50 -      val Simpset ({bounds = (_, bounds), ...}, _) = simpset_of ctxt;
    1.51 -      val bs =
    1.52 -        fold_aterms
    1.53 -          (fn Free (x, _) =>
    1.54 -            if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
    1.55 -            then insert (op =) x else I
    1.56 -          | _ => I) (term_of ct) [];
    1.57 -    in
    1.58 -      if null bs then ()
    1.59 -      else
    1.60 -        print_term ctxt true
    1.61 -          (fn () => "Simplifier: term contains loose bounds: " ^ commas_quote bs)
    1.62 -          (Thm.term_of ct)
    1.63 -    end
    1.64 -  else ();
    1.65 -
    1.66  fun rewrite_cterm mode prover raw_ctxt raw_ct =
    1.67    let
    1.68      val thy = Proof_Context.theory_of raw_ctxt;
    1.69 @@ -1359,7 +1339,6 @@
    1.70        |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
    1.71  
    1.72      val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
    1.73 -    val _ = check_bounds ctxt ct;
    1.74    in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
    1.75  
    1.76  val simple_prover =