1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 08 22:17:52 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 08 22:17:52 2010 +0100
     1.3 @@ -370,7 +370,7 @@
     1.4      val problem =
     1.5        {state = st', goal = goal, subgoal = i,
     1.6         subgoal_count = Sledgehammer_Util.subgoal_count st,
     1.7 -       facts = facts |> map Sledgehammer_Provers.Untranslated}
     1.8 +       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
     1.9      val time_limit =
    1.10        (case hard_timeout of
    1.11          NONE => I