src/CCL/Term.thy

--- a/src/CCL/Term.thy	Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Term.thy	Wed Oct 03 21:29:05 2007 +0200
@@ -31,7 +31,7 @@
   nrec       :: "[i,i,[i,i]=>i]=>i"
 
   nil        :: "i"                        ("([])")
-  "$"        :: "[i,i]=>i"                 (infixr 80)
+  cons       :: "[i,i]=>i"                 (infixr "$" 80)
   lcase      :: "[i,i,[i,i]=>i]=>i"
   lrec       :: "[i,i,[i,i,i]=>i]=>i"
 
@@ -288,7 +288,7 @@
 ML_setup {*
 bind_thms ("term_dstncts",
   mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
-    [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","op $"]]);
+    [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
 *}