src/Tools/Code/code_runtime.ML
changeset 59104 a14475f044b2
parent 58645 94bef115c08f
child 59127 723b11f8ffbf
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Dec 04 16:51:54 2014 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Dec 05 19:35:36 2014 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  datatype truth = Holds;
     1.5  
     1.6  val _ = Theory.setup
     1.7 -  (Code_Target.extend_target (target, (Code_ML.target_SML, I))
     1.8 +  (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
     1.9    #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
    1.10      [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
    1.11    #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},