| changeset 20593 | 5af400cc64d5 |
| parent 17604 | 5f30179fbf44 |
| child 20637 | d883e0fc1c51 |
--- a/src/HOL/Extraction/Higman.thy Tue Sep 19 15:21:51 2006 +0200 +++ b/src/HOL/Extraction/Higman.thy Tue Sep 19 15:21:52 2006 +0200 @@ -294,6 +294,9 @@ contains test = good_prefix +declare barT.recs(2) [where ?fun = ?func, code func] +code_gen good_prefix (SML _) (SML "~~/src/codegen/generated/higman.ML") + ML {* local open Higman in