equal
deleted
inserted
replaced
77 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj" |
77 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj" |
78 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI'); |
78 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI'); |
79 val {ppc, where_, prls, ...} = Problem.from_store pID; |
79 val {ppc, where_, prls, ...} = Problem.from_store pID; |
80 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty |
80 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty |
81 then (false, (I_Model.init ppc, [])) |
81 then (false, (I_Model.init ppc, [])) |
82 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris; |
82 else Model.match_itms_oris thy itms (ppc, where_, prls) oris; |
83 in |
83 in |
84 Applicable.Yes (Tactic.Specify_Problem' (pID, pbl)) |
84 Applicable.Yes (Tactic.Specify_Problem' (pID, pbl)) |
85 end |
85 end |
86 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI) |
86 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI) |
87 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable" |
87 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable" |