110 fun check_free ts (orient, Free f) |
110 fun check_free ts (orient, Free f) |
111 = if not check_frees orelse not orient |
111 = if not check_frees orelse not orient |
112 orelse exists (curry Logic.occs (Free f)) ts |
112 orelse exists (curry Logic.occs (Free f)) ts |
113 then (orient, true) else raise Match |
113 then (orient, true) else raise Match |
114 | check_free ts (orient, _) = (orient, false) |
114 | check_free ts (orient, _) = (orient, false) |
115 fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs |
115 fun eq_var_aux k \<^Const_>\<open>Pure.all _ for \<open>Abs(_,_,t)\<close>\<close> hs = eq_var_aux k t hs |
116 | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) hs = |
116 | eq_var_aux k \<^Const_>\<open>Pure.imp for A B\<close> hs = |
117 ((k, check_free (B :: hs) (inspect_pair bnd novars |
117 ((k, check_free (B :: hs) (inspect_pair bnd novars |
118 (Data.dest_eq (Data.dest_Trueprop A)))) |
118 (Data.dest_eq (Data.dest_Trueprop A)))) |
119 handle TERM _ => eq_var_aux (k+1) B (A :: hs) |
119 handle TERM _ => eq_var_aux (k+1) B (A :: hs) |
120 | Match => eq_var_aux (k+1) B (A :: hs)) |
120 | Match => eq_var_aux (k+1) B (A :: hs)) |
121 | eq_var_aux k _ _ = raise EQ_VAR |
121 | eq_var_aux k _ _ = raise EQ_VAR |