1.1 --- a/src/HOL/Tools/meson.ML	Mon Sep 29 10:58:04 2008 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Sep 29 11:46:47 2008 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4        val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
     1.5        val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
     1.6    in  thA RS (cterm_instantiate ct_pairs thB)  end
     1.7 -  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
     1.8 +  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);  (* FIXME avoid handle _ *)
     1.9  
    1.10  fun flexflex_first_order th =
    1.11    case (tpairs_of th) of