equal
deleted
inserted
replaced
49 else error "scrtools.sml: contain_bdv doesnt work for 'integration'"; |
49 else error "scrtools.sml: contain_bdv doesnt work for 'integration'"; |
50 |
50 |
51 if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]" |
51 if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]" |
52 then () else error "formal_args of auto-gen.script changed"; |
52 then () else error "formal_args of auto-gen.script changed"; |
53 |
53 |
54 Istate.init_detail ctxt (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.parse_test @{context} "someTermWithBdv"); |
54 Istate.init_detail ctxt (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (ParseC.parse_test @{context} "someTermWithBdv"); |
55 "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t) |
55 "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t) |
56 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.parse_test @{context} "someTermWithBdv"); |
56 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), ParseC.parse_test @{context} "someTermWithBdv"); |
57 val v = case Tactic.subst_adapt_to_type ctxt subs of |
57 val v = case Tactic.subst_adapt_to_type ctxt subs of |
58 (_, v) :: _ => v; |
58 (_, v) :: _ => v; |
59 (*case*) get_rls ctxt rls (*of*); |
59 (*case*) get_rls ctxt rls (*of*); |
60 |
60 |
61 |
61 |