src/HOL/Tools/numeral_syntax.ML
changeset 15013 34264f5e4691
parent 14981 e73f8140af78
child 15595 dc8a41c7cefc
--- a/src/HOL/Tools/numeral_syntax.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -28,8 +28,8 @@
   | prefix_len pred (x :: xs) =
       if pred x then 1 + prefix_len pred xs else 0;
 
-fun bin_of (Const ("bin.Pls", _)) = []
-  | bin_of (Const ("bin.Min", _)) = [~1]
+fun bin_of (Const ("Numeral.Pls", _)) = []
+  | bin_of (Const ("Numeral.Min", _)) = [~1]
   | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of _ = raise Match;
 
@@ -70,7 +70,7 @@
 (* theory setup *)
 
 val setup =
- [Theory.hide_consts false ["Numeral.bin.Pls", "Numeral.bin.Min"],
+ [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];