src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 42344 4a58173ffb99
parent 42342 6babd86a54a4
child 42348 187354e22c7d
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -652,8 +652,9 @@
     1.4        | (Var _, _) => add_terms (t, u)
     1.5        | (_, Var _) => add_terms (u, t)
     1.6        | _ => I
     1.7 -    val t_inst = [] |> unify_terms (prem, concl)
     1.8 -                    |> map (pairself (cterm_of thy))
     1.9 +    val t_inst =
    1.10 +      [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
    1.11 +         |> the_default [] (* FIXME *)
    1.12    in th |> cterm_instantiate t_inst end
    1.13  
    1.14  val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}