1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 11:55:16 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 14:05:55 2016 +0100
1.3 @@ -32,7 +32,7 @@
1.4 val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
1.5 val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
1.6 val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac
1.7 - val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy
1.8 + val context_thy : Ctree.state -> Ctree.tac -> contthy
1.9 val distinct_Thm : rule list -> rule list
1.10 val eq_Thms : string list -> rule -> bool
1.11 val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->