--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 18:24:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 18:31:45 2010 +0200
@@ -55,7 +55,7 @@
max_relevant = NONE, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
val axioms =
- axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))
+ axioms |> maps (fn (n, ths) => ths |> map (Untranslated o pair n))
val {goal, ...} = Proof.goal state
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,