changeset 20637 | d883e0fc1c51 |
parent 20593 | 5af400cc64d5 |
child 20837 | 099877d83d2b |
--- a/src/HOL/Extraction/Higman.thy Wed Sep 20 09:08:35 2006 +0200 +++ b/src/HOL/Extraction/Higman.thy Wed Sep 20 10:13:36 2006 +0200 @@ -295,7 +295,7 @@ test = good_prefix declare barT.recs(2) [where ?fun = ?func, code func] -code_gen good_prefix (SML _) (SML "~~/src/codegen/generated/higman.ML") +code_gen good_prefix (SML -) ML {* local open Higman in