diff -r d56b817fbb14 -r 141f72881af7 src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 23 09:42:19 2018 +0200
+++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 23 11:01:03 2018 +0200
@@ -40,13 +40,14 @@
 *}
 
 subsection {* Type 'xlist' for Lucas-Interpretation *}
-(*TODO: ask for shorter deliminters in xlist *)
-datatype 'a xlist =
-    XNil    ("{|| ||}")
-  | XCons 'a  "'a xlist"    (infixr "@#" 65)
+(* cp fom ~~/src/HOL/List.thy
+   TODO: ask for shorter deliminters in xlist *)
+datatype  'a xlist =
+    XNil  ("{|| ||}")
+  | XCons (xhd: 'a)  (xtl: "'a xlist")  (infixr "@#" 65)
 
 syntax
-  -- {* list Enumeration *}
+   \<comment> \<open>list Enumeration\<close>
   "_xlist" :: "args => 'a xlist"    ("{|| (_) ||}")
 
 translations
@@ -78,6 +79,7 @@
 NTH_NIL: "NTH 1 (x # xs) = x" and
 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
 
+(* redefine together with identifiers (still) required for KEStore ..*)
 axiomatization where
 hd_thm:	"hd (x # xs) = x"