diff -r a2a89563bfcb -r 4202e11ae7dc src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Tue Jun 15 07:42:48 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Tue Jun 15 08:32:32 2010 +0200 @@ -55,7 +55,7 @@ val value_name = "Value.VALUE.value" val program' = program |> Graph.new_node (value_name, - Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))]))) + Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE))) |> fold (curry Graph.add_edge value_name) deps; val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy (the_default target some_target) "" naming program' [value_name];