src/HOL/Import/shuffler.ML
changeset 28397 389c5e494605
parent 27865 27a8ad9612a3
child 29265 5b4247055bd7
     1.1 --- a/src/HOL/Import/shuffler.ML	Mon Sep 29 10:58:04 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Mon Sep 29 11:46:47 2008 +0200
     1.3 @@ -66,14 +66,14 @@
     1.4           Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
     1.5         | Const("==",_) $ _ $ _ => th
     1.6         | _ => raise THM("Not an equality",0,[th]))
     1.7 -    handle _ => raise THM("Couldn't make meta equality",0,[th])
     1.8 +    handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
     1.9  
    1.10  fun mk_obj_eq th =
    1.11      (case concl_of th of
    1.12           Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
    1.13         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
    1.14         | _ => raise THM("Not an equality",0,[th]))
    1.15 -    handle _ => raise THM("Couldn't make object equality",0,[th])
    1.16 +    handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
    1.17  
    1.18  structure ShuffleData = TheoryDataFun
    1.19  (