equal
deleted
inserted
replaced
43 (**) |
43 (**) |
44 datatype T = datatype Rule_Def.rule_set; |
44 datatype T = datatype Rule_Def.rule_set; |
45 type id = string; |
45 type id = string; |
46 |
46 |
47 (*/------- this will disappear eventually ----------------------------------------------------\*) |
47 (*/------- this will disappear eventually ----------------------------------------------------\*) |
48 fun dummy_ord (_: (term * term) list) (_: term, _: term) = true; |
48 fun dummy_ord (_: LibraryC.subst) (_: term, _: term) = true; |
49 val empty = |
49 val empty = |
50 Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty, |
50 Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty, |
51 srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.Empty_Prog} |
51 srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.Empty_Prog} |
52 (*\------- this will disappear eventually ----------------------------------------------------/*) |
52 (*\------- this will disappear eventually ----------------------------------------------------/*) |
53 |
53 |