--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
@@ -325,10 +325,10 @@
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
- val css_table = clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts =
refs |> maps (map (apsnd single)
- o fact_from_ref ctxt reserved chained_ths css_table)
+ o fact_from_ref ctxt reserved chained_ths css)
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"