1080 and subc skel ctxt t0 = |
1080 and subc skel ctxt t0 = |
1081 let val Simpset (_, {congs, ...}) = simpset_of ctxt in |
1081 let val Simpset (_, {congs, ...}) = simpset_of ctxt in |
1082 (case term_of t0 of |
1082 (case term_of t0 of |
1083 Abs (a, T, _) => |
1083 Abs (a, T, _) => |
1084 let |
1084 let |
1085 val (b, ctxt') = Variable.next_bound (a, T) ctxt; |
1085 val (v, ctxt') = Variable.next_bound (a, T) ctxt; |
1086 val (v, t') = Thm.dest_abs (SOME b) t0; |
1086 val b = #1 (Term.dest_Free v); |
1087 val b' = #1 (Term.dest_Free (term_of v)); |
1087 val (v', t') = Thm.dest_abs (SOME b) t0; |
|
1088 val b' = #1 (Term.dest_Free (term_of v')); |
1088 val _ = |
1089 val _ = |
1089 if b <> b' then |
1090 if b <> b' then |
1090 warning ("Simplifier: renamed bound variable " ^ |
1091 warning ("Bad Simplifier context: renamed bound variable " ^ |
1091 quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) |
1092 quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) |
1092 else (); |
1093 else (); |
1093 val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0); |
1094 val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0); |
1094 in |
1095 in |
1095 (case botc skel' ctxt' t' of |
1096 (case botc skel' ctxt' t' of |
1096 SOME thm => SOME (Thm.abstract_rule a v thm) |
1097 SOME thm => SOME (Thm.abstract_rule a v' thm) |
1097 | NONE => NONE) |
1098 | NONE => NONE) |
1098 end |
1099 end |
1099 | t $ _ => |
1100 | t $ _ => |
1100 (case t of |
1101 (case t of |
1101 Const ("==>", _) $ _ => impc t0 ctxt |
1102 Const ("==>", _) $ _ => impc t0 ctxt |