src/HOL/Statespace/DistinctTreeProver.thy
changeset 42287 d98eb048a2e4
parent 39557 fe5722fce758
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Apr 08 14:05:31 2011 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Apr 08 14:20:57 2011 +0200
     1.3 @@ -643,8 +643,7 @@
     1.4  *)
     1.5  val nums = (0 upto 10000);
     1.6  val nums' = (0 upto 3000);
     1.7 -val const_decls = map (fn i => Syntax.no_syn 
     1.8 -                                 ("const" ^ string_of_int i,Type ("nat",[]))) nums
     1.9 +val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums
    1.10  
    1.11  val consts = sort Term_Ord.fast_term_ord 
    1.12                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)