# HG changeset patch # User wenzelm # Date 1425672867 -3600 # Node ID a6e977d8b0709413a23cd9761adf51642ce398d7 # Parent aacdce52b2fce4f0b110a3b4a2c49c41026db377 clarified context; diff -r aacdce52b2fc -r a6e977d8b070 src/ZF/Tools/cartprod.ML --- a/src/ZF/Tools/cartprod.ML Fri Mar 06 20:08:45 2015 +0100 +++ b/src/ZF/Tools/cartprod.ML Fri Mar 06 21:14:27 2015 +0100 @@ -106,10 +106,10 @@ fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) = let val T' = factors T1 ---> T2 val newt = ap_split T1 T2 (Var(v,T')) - val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl) in - remove_split ctxt (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), - cterm newt)]) rl) + remove_split ctxt + (Drule.instantiate_normalize ([], + [apply2 (Thm.cterm_of ctxt) (Var(v, Ind_Syntax.iT-->T2), newt)]) rl) end | split_rule_var _ (t,T,rl) = rl; diff -r aacdce52b2fc -r a6e977d8b070 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Fri Mar 06 20:08:45 2015 +0100 +++ b/src/ZF/Tools/ind_cases.ML Fri Mar 06 21:14:27 2015 +0100 @@ -30,6 +30,7 @@ fun smart_cases ctxt s = let val thy = Proof_Context.theory_of ctxt; + fun err msg = cat_error msg ("Malformed set membership statement: " ^ s); val A = Syntax.read_prop ctxt s handle ERROR msg => err msg; val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop @@ -37,7 +38,7 @@ in (case Symtab.lookup (IndCasesData.get thy) c of NONE => error ("Unknown inductive cases rule for set " ^ quote c) - | SOME f => f ctxt (Thm.global_cterm_of thy A)) + | SOME f => f ctxt (Thm.cterm_of ctxt A)) end;