equal
deleted
inserted
replaced
38 val pres = map (mk_env probl |> subst_atomic) where_; |
38 val pres = map (mk_env probl |> subst_atomic) where_; |
39 (*val pres = mk_env pbl |> subst_atomic #> where_;*) |
39 (*val pres = mk_env pbl |> subst_atomic #> where_;*) |
40 if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then () |
40 if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then () |
41 else error "appl.sml Apply_Method diff.behav."; |
41 else error "appl.sml Apply_Method diff.behav."; |
42 |
42 |
43 val ctxt = assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres; |
43 val ctxt = assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres; |
44 (*TODO.WN110416 read pres from ctxt and check*) |
44 (*TODO.WN110416 read pres from ctxt and check*) |
45 |
45 |
46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
47 show_pt pt; |
47 show_pt pt; |
48 |
48 |