src/Tools/isac/Interpret/rewtools.sml
changeset 59281 bcfca6e8b79e
parent 59279 255c853ea2f0
child 59291 354be0aa3cc5
     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) ->