equal
deleted
inserted
replaced
39 | Ctree.ModSpec (_, p_, _, gfr, pre, _) => |
39 | Ctree.ModSpec (_, p_, _, gfr, pre, _) => |
40 Generate.PpcKF ( |
40 Generate.PpcKF ( |
41 (case p_ of Pos.Pbl => Generate.Problem [] |
41 (case p_ of Pos.Pbl => Generate.Problem [] |
42 | Pos.Met => Generate.Method [] |
42 | Pos.Met => Generate.Method [] |
43 | _ => error "TESTg_form: uncovered case", |
43 | _ => error "TESTg_form: uncovered case", |
44 Specify.itms2itemppc (Celem.assoc_thy"Isac_Knowledge") gfr pre)) |
44 Specify.itms2itemppc (ThyC.get_theory"Isac_Knowledge") gfr pre)) |
45 end |
45 end |
46 (* for quick test-print-out, until 'type inout' is removed *) |
46 (* for quick test-print-out, until 'type inout' is removed *) |
47 fun f2str (Generate.FormKF cterm') = cterm' |
47 fun f2str (Generate.FormKF cterm') = cterm' |
48 | f2str _ = error "f2str: uncovered case in fun.def."; |
48 | f2str _ = error "f2str: uncovered case in fun.def."; |
49 |
49 |