--- a/src/HOL/Sexp.thy Tue Jun 04 12:49:04 1996 +0200
+++ b/src/HOL/Sexp.thy Thu Jun 06 13:13:18 1996 +0200
@@ -18,7 +18,7 @@
pred_sexp :: "('a item * 'a item)set"
-inductive "sexp"
+inductive sexp
intrs
LeafI "Leaf(a): sexp"
NumbI "Numb(i): sexp"
--- a/src/HOL/thy_syntax.ML Tue Jun 04 12:49:04 1996 +0200
+++ b/src/HOL/thy_syntax.ML Thu Jun 06 13:13:18 1996 +0200
@@ -84,7 +84,7 @@
val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
in
- repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
+ repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
>> mk_params
end;