equal
deleted
inserted
replaced
271 additions. |
271 additions. |
272 *} |
272 *} |
273 |
273 |
274 ML{*fun term_tree n = |
274 ML{*fun term_tree n = |
275 let |
275 let |
276 val count = ref 0; |
276 val count = Unsynchronized.ref 0; |
277 |
277 |
278 fun term_tree_aux n = |
278 fun term_tree_aux n = |
279 case n of |
279 case n of |
280 0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count)) |
280 0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count)) |
281 | _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) |
281 | _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) |