--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 21:01:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 21:34:01 2010 +0200
@@ -141,8 +141,7 @@
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
val facts =
- maps (map (apsnd single)
- o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
+ maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) refs
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"