# HG changeset patch
# User wenzelm
# Date 979326240 -3600
# Node ID 405b077433a3a129b35f5b78a92b673fe8e09547
# Parent  890b117f61898ad9c44d539cd31cf7477193a64a
HOLogic.dest_binum;
avoid handle _ !!!

diff -r 890b117f6189 -r 405b077433a3 src/HOL/Tools/svc_funcs.ML
--- a/src/HOL/Tools/svc_funcs.ML	Fri Jan 12 20:03:26 2001 +0100
+++ b/src/HOL/Tools/svc_funcs.ML	Fri Jan 12 20:04:00 2001 +0100
@@ -74,8 +74,10 @@
 			File.sysify_path svc_output_file ^
 			" " ^ File.sysify_path svc_input_file ^ 
 			"> /dev/null 2>&1"))
-      val svc_output = File.read svc_output_file
-	               handle _ => error "SVC returned no output"
+      val svc_output =
+        (case Library.try File.read svc_output_file of
+          Some out => out
+        | None => error "SVC returned no output");
   in
       if ! trace then writeln ("SVC Returns:\n" ^ svc_output)
       else (File.rm svc_input_file; File.rm svc_output_file);
@@ -150,7 +152,8 @@
                become part of the Var's name*)
       | var (t,_) = raise OracleExn t;
     (*translation of a literal*)
-    fun lit (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w
+    fun lit (Const("Numeral.number_of", _) $ w) =
+          (HOLogic.dest_binum w handle TERM _ => raise Match)
       | lit (Const("0", _)) = 0
       | lit (Const("RealDef.0r", _)) = 0
       | lit (Const("RealDef.1r", _)) = 1