src/Pure/raw_simplifier.ML
changeset 46707 1427dcc7c9a6
parent 46465 5ba52c337cd0
child 47239 0b1829860149
equal deleted inserted replaced
46706:877d57975427 46707:1427dcc7c9a6
  1307   let val ss = empty_ss addsimps rews in
  1307   let val ss = empty_ss addsimps rews in
  1308     fn i => fn st => generic_rewrite_goal_tac (true, false, false) (K no_tac)
  1308     fn i => fn st => generic_rewrite_goal_tac (true, false, false) (K no_tac)
  1309       (global_context (Thm.theory_of_thm st) ss) i st
  1309       (global_context (Thm.theory_of_thm st) ss) i st
  1310   end;
  1310   end;
  1311 
  1311 
  1312 (*Prunes all redundant parameters from the proof state by rewriting.
  1312 (*Prunes all redundant parameters from the proof state by rewriting.*)
  1313   DOES NOT rewrite main goal, where quantification over an unused bound
       
  1314     variable is sometimes done to avoid the need for cut_facts_tac.*)
       
  1315 val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
  1313 val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
  1316 
  1314 
  1317 
  1315 
  1318 (* for folding definitions, handling critical pairs *)
  1316 (* for folding definitions, handling critical pairs *)
  1319 
  1317