equal
deleted
inserted
replaced
436 else raise TEST lthy6 |
436 else raise TEST lthy6 |
437 |
437 |
438 val qtys = map #qtyp qty_infos |
438 val qtys = map #qtyp qty_infos |
439 |
439 |
440 (* defining of quotient term-constructors, binding functions, free vars functions *) |
440 (* defining of quotient term-constructors, binding functions, free vars functions *) |
441 val _ = warning "Defining the quotient constnats" |
441 val _ = warning "Defining the quotient constants" |
442 val qconstrs_descr = |
442 val qconstrs_descr = |
443 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
443 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
444 |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs |
444 |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs |
445 |
445 |
446 val qbns_descr = |
446 val qbns_descr = |