equal
deleted
inserted
replaced
148 and subst_termify (Abs (v, T, t)) = (case subst_termify t |
148 and subst_termify (Abs (v, T, t)) = (case subst_termify t |
149 of SOME t' => SOME (Abs (v, T, t')) |
149 of SOME t' => SOME (Abs (v, T, t')) |
150 | NONE => NONE) |
150 | NONE => NONE) |
151 | subst_termify t = subst_termify_app (strip_comb t) |
151 | subst_termify t = subst_termify_app (strip_comb t) |
152 |
152 |
153 fun check_termify ts ctxt = map_default subst_termify ts |
153 fun check_termify ctxt ts = |
154 |> Option.map (rpair ctxt) |
154 the_default ts (map_default subst_termify ts); |
155 |
155 |
156 |
156 |
157 (** evaluation **) |
157 (** evaluation **) |
158 |
158 |
159 structure Evaluation = Proof_Data |
159 structure Evaluation = Proof_Data |