equal
deleted
inserted
replaced
137 fun tryabsdecomp (ct, ctxt) bds = |
137 fun tryabsdecomp (ct, ctxt) bds = |
138 (case Thm.term_of ct of |
138 (case Thm.term_of ct of |
139 Abs (_, xT, ta) => |
139 Abs (_, xT, ta) => |
140 let |
140 let |
141 val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt; |
141 val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt; |
142 val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta); (* FIXME !? *) |
142 val (xn, ta) = Term.dest_abs (raw_xn, xT, ta); |
143 val x = Free (xn, xT); |
143 val x = Free (xn, xT); |
144 val cx = Thm.cterm_of ctxt' x; |
144 val cx = Thm.cterm_of ctxt' x; |
145 val cta = Thm.cterm_of ctxt' ta; |
145 val cta = Thm.cterm_of ctxt' ta; |
146 val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of |
146 val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of |
147 NONE => error "tryabsdecomp: Type not found in the Environement" |
147 NONE => error "tryabsdecomp: Type not found in the Environement" |