author | haftmann |
Wed, 20 Sep 2006 10:13:36 +0200 | |
changeset 20637 | d883e0fc1c51 |
parent 20636 | ddddf0b7d322 |
child 20638 | 241792a4634e |
--- 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