1.1 --- a/src/Tools/isac/Specify/generate.sml	Sat May 02 09:15:39 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/generate.sml	Sat May 02 10:57:04 2020 +0200
     1.3 @@ -245,16 +245,6 @@
     1.4      in
     1.5        ((p, Res), c, FormKF (UnparseC.term f'), pt)
     1.6      end
     1.7 -  | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, _)) (is, ctxt) (pt, (p, _)) =
     1.8 -    let
     1.9 -      val (pt, _) = cappend_form pt p (is, ctxt) f 
    1.10 -      val pt = update_branch pt p TransitiveB
    1.11 -      val is = init_istate (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs, Rule_Set.id rls)) f 
    1.12 -      val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
    1.13 -      val pos' = ((lev_on o lev_dn) p, Frm)
    1.14 -    in
    1.15 -      generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
    1.16 -    end
    1.17    | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
    1.18      let
    1.19        val (pt, c) = cappend_atomic pt p (is, ctxt) f 
    1.20 @@ -263,16 +253,6 @@
    1.21      in
    1.22        ((p, Res), c, FormKF (UnparseC.term f'), pt)
    1.23      end
    1.24 -  | generate1 (Tactic.Detail_Set' (_, _, rls, f, _)) (is, ctxt) (pt, (p, _)) =
    1.25 -    let
    1.26 -      val (pt, _) = cappend_form pt p (is, ctxt) f 
    1.27 -      val pt = update_branch pt p TransitiveB
    1.28 -      val is = init_istate (Tactic.Rewrite_Set (Rule_Set.id rls)) f
    1.29 -      val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
    1.30 -      val pos' = ((lev_on o lev_dn) p, Frm)
    1.31 -    in
    1.32 -      generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
    1.33 -    end
    1.34    | generate1 (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
    1.35        let
    1.36          val (pt, c) = append_result pt p l (scval, []) Complete