"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
authorblanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 423444a58173ffb99
parent 42343 118cc349de35
child 42345 5ecd55993606
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
src/HOL/Tools/Metis/metis_reconstruct.ML
     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}