equal
deleted
inserted
replaced
30 if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then () |
30 if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then () |
31 else raise ERROR "theory dependencies not as anticipated in ThyC" |
31 else raise ERROR "theory dependencies not as anticipated in ThyC" |
32 end |
32 end |
33 \<close> ML \<open> |
33 \<close> ML \<open> |
34 \<close> ML \<open> |
34 \<close> ML \<open> |
|
35 \<close> ML \<open> |
|
36 fun tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) = |
|
37 let |
|
38 val tid = HOLogic.dest_string thmID |
|
39 val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub |
|
40 in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end |
|
41 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) = |
|
42 (Tactic.Rewrite_Set (HOLogic.dest_string rls)) |
|
43 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) = |
|
44 let |
|
45 val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub |
|
46 in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end |
|
47 \<close> ML \<open> |
|
48 \<close> ML \<open> |
|
49 \<close> ML \<open> |
35 \<close> |
50 \<close> |
36 end |
51 end |