src/ZF/Datatype.ML
changeset 7693 c3e0c26e7d6f
parent 6141 a6922171b396
child 9000 c20d58286a51
equal deleted inserted replaced
7692:89bbce6f5c17 7693:c3e0c26e7d6f
    57 
    57 
    58   val trace = ref false;
    58   val trace = ref false;
    59 
    59 
    60   fun mk_new ([],[]) = Const("True",FOLogic.oT)
    60   fun mk_new ([],[]) = Const("True",FOLogic.oT)
    61     | mk_new (largs,rargs) =
    61     | mk_new (largs,rargs) =
    62 	fold_bal (app FOLogic.conj) 
    62 	fold_bal FOLogic.mk_conj
    63 		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    63 		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    64 
    64 
    65 
    65 
    66  fun proc sg _ old =
    66  fun proc sg _ old =
    67    let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    67    let val _ = if !trace then writeln ("data_free: OLD = " ^