changeset 48292 | 7fcee834c7f5 |
parent 48250 | 1065c307fafe |
child 48293 | 914ca0827804 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:03 2012 +0200 @@ -327,7 +327,7 @@ let val ctxt = Proof.context_of state val reserved = reserved_isar_keyword_table () - val chained_ths = normalize_chained_theorems (#facts (Proof.goal state)) + val chained_ths = #facts (Proof.goal state) val css_table = clasimpset_rule_table_of ctxt val facts = refs |> maps (map (apsnd single)