404 |
404 |
405 (* definition of raw fv_functions *) |
405 (* definition of raw fv_functions *) |
406 val lthy3 = Theory_Target.init NONE thy; |
406 val lthy3 = Theory_Target.init NONE thy; |
407 val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; |
407 val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; |
408 |
408 |
409 val ((fv, fvbn), fv_def, lthy3a) = |
409 val (fv, fvbn, fv_def, lthy3a) = |
410 if get_STEPS lthy2 > 3 |
410 if get_STEPS lthy2 > 3 |
411 then define_raw_fv descr sorts raw_bns raw_bclauses lthy3 |
411 then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3 |
412 else raise TEST lthy3 |
412 else raise TEST lthy3 |
413 |
413 |
414 |
|
415 (* definition of raw alphas *) |
414 (* definition of raw alphas *) |
416 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
415 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
417 if get_STEPS lthy > 4 |
416 if get_STEPS lthy > 4 |
418 then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a |
417 then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a |
419 else raise TEST lthy3a |
418 else raise TEST lthy3a |